cannot locate theory in included dir

[cassiersg]

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]

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]

Indeed.

[fdupress]

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]

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]

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]

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

[strub]

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

[fdupress]

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