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

[petithug]

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.

[gallais]

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?

[jfdm]

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.

[petithug]

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.