Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cannot locate theory in included dir #659

Closed
cassiersg opened this issue Nov 4, 2024 · 11 comments · Fixed by #663
Closed

cannot locate theory in included dir #659

cassiersg opened this issue Nov 4, 2024 · 11 comments · Fixed by #663
Assignees
Labels

Comments

@cassiersg
Copy link
Contributor

It seems that if a directory is included with the -I flag (or idirs in easycrypt.conf), then it cannot be accessed as a direct "local" require anymore.

To reproduce:

  1. Create empty file a.ec
  2. Create b.ec with content require import A.
  3. easycrypt b.ec works
  4. but easycrypt -IX:$(realpath .) b.ec fails with error message
[critical] [: line 1 (0) to line 2 (17)] cannot locate theory `A'

This is annoying when simultaneously (i.e., using the same easycrypt config) developing a library and testing its use.

@fdupress
Copy link
Member

fdupress commented Nov 4, 2024

This is only a problem if you namespace the include, right? (in other words: your command works if you do not include the X: portion of it?)

@cassiersg
Copy link
Contributor Author

Indeed.

@fdupress
Copy link
Member

fdupress commented Nov 5, 2024

Alright, so I had looked into this about a year back, and could not think of a workflow that would make this a bug rather than a quirk.

It is, in fact, quite a bit more complex than the situation you describe because of interactions between namespacing and recursive loadpath—you could -R folder and -I X:folder/subfolder, for example; or -I X:folder and -I Y:folder, or all sorts of weirdly tangled namespace knots. (I also have no clue how this interacts with symbolic links.)

It made sense to me at the time that a decision had been made (theories included in namespaced loads are not accessible without namespace, non-recursive namespaced loads take precedence over recursive namespaced loads, namespaced loads at the same level of recursiveness are processed earliest-first), that it was being applied consistently across all ways of extending the loadpath, and that it only needed to be documented. (Which, of course, I didn't do—sorry!)

I really do not see a change that would make a single theory accessible as two different names as good. But I'm not sure the view is entirely with merit.

@cassiersg
Copy link
Contributor Author

For more context on my workflow: I am developing jasmin's eclib, which I also want to use (to test it).

There are of course multiple fairly easy ways for me to work around the issue. The most annoying is probably the not-so-informative error message, on top of a somewhat surprising behavior: I didn't expect that adding a directory to what looks like a "search path" would make files "disappear" (and that wasn't helped by having the -I directive be actually a idirs in ~/.config/easycrypt/easycrypt.conf set long ago...) .

Regarding the fundamental issue of having a single theory accessible under two different names, I'm not sure if that would be a problem for easycrypt.

@strub strub self-assigned this Nov 6, 2024
@strub
Copy link
Member

strub commented Nov 12, 2024

The namespacing implementation of EC needs to be revisited -- we currently do not keep the namespace information internally. I'll see if I can fix this issue quickly though.

@fdupress
Copy link
Member

Perhaps a first bit of progress here would be for easycrypt config to display the source of a each line in the loadpath?

@strub
Copy link
Member

strub commented Nov 12, 2024

What do you mean by "the source of each line"?

@fdupress
Copy link
Member

Whether a path was added by command line, easycrypt.config or easycrypt.project.

@strub
Copy link
Member

strub commented Dec 2, 2024

Back to this: this is a bug. When adding a directory to the include path, that is a duplicate check. However, this check does not take the namespace into account.

@strub strub added the bug label Dec 2, 2024
@strub strub linked a pull request Dec 2, 2024 that will close this issue
@strub
Copy link
Member

strub commented Dec 2, 2024

@cassiersg Can you check that you are happy with the fix?

@cassiersg
Copy link
Contributor Author

@strub Yes, it fixes my issue. Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants