Idris always use <file>.idr instead of <file>.lidr

[edwinb]

Issue by petithug
Sunday Mar 29, 2020 at 17:54 GMT
Originally opened as edwinb/Idris2-boot#246

---

This is a corner case, but an annoying one when migrating idris1 files to literate idris2 files.

Steps to Reproduce

Crete two files with the same name, different content, but one with the ".idr" extension and the other with the ".lidr" extension.

Expected Behavior

Loading each file in the REPL will create different build/ content.

Observed Behavior

When loading the ".lidr" file, the ".idr file is used instead, and build/ contains the same content than for the ".idr" file.

[edwinb]

Comment by gallais
Wednesday Apr 01, 2020 at 13:48 GMT

---

AFAIU this is more a problem of seeing an existing .ttc and loading it despite
the fact it has been generated from the .idr and not the .lidr file. What I
find strange is that, surely, we have a mechanism to detect whether a file has
been updated since the last time the .ttc was generated and it should kick in
here and provoke re-compilation?

[edwinb]

Comment by jfdm
Wednesday Apr 01, 2020 at 20:31 GMT

---

From a quick look over the source, I think the issue here is that Idris2 generates a ttc file with the file's basename. Thus, when given a literate idris file and ordinary idris file with the same basename, as per the above example, then Idris will default to the ordinary file.

See:

https://github.com/edwinb/Idris2/blob/master/src/Idris/ProcessIdr.idr#L313
https://github.com/edwinb/Idris2/blob/2c2acdcfacc230ccf8da145097af903b3df5b56a/src/Core/Directory.idr#L169

I am not sure if Idris1 has the same issue and how it dealt with it, if there was no issue.

[edwinb]

Comment by petithug
Sunday Apr 05, 2020 at 19:31 GMT

---

I do not think the presence of the ttc file is the problem:

In a clean directory creates two files, a Test.idr containing module test (so it is incorrect) and a Test.lidr containing > module Test (so it is correct).

Then run idris2 Test.lidr. It says that the module name does not match the filename whichcab ne only because Test.idr is loaded instead. Remove Test.idr and everything work fine.

[gallais]

Looking at something else, I think I have accidentally found the origin of this:

• getBuildMods computes the module name associated to the main file using pathToNS
• mkModTree computes back the file path using the module name via nsToSource
• nsToSource calls firstAvailable prioritising .idr over .lidr

I should have a fix fairly soon if that's indeed the issue.