Improve idris-filename-to-load to return expected pair of dir and relative path depending on idris-protocol version

[keram]

What:

Make (idris-filename-to-load) to return

• a "source dir" and "relative file path" when source dir is exctracted from ipkg file.
• a "work dir" (parent directory containing a ipkg file) and "relative file path" when Idris protocol version is greater than 1.
• a "parent directory" and "file" when no ipkg file found

Why:

In Idris2 the files are loaded relative to work directory which is a directory containing an ".ipkg" file.
This will allow us reintroduce regexp to correctly extract sourcedir value from ipkg file in Idris2.

Relates to:
idris-lang/Idris2#3310
#627

[jfdm]

AFAICT, the error is due to flycheck. I am not sure how your changes would have triggered the flycheck eror, I suspect they didn't.

I will run the builds again and hope for the best...

[jfdm]

Ahh, the flycheck things are warnings.

The issue seems to be:

 In toplevel form:
idris-commands.el:1390:1:Error: the function ‘file-name-parent-directory’ is not known to be defined.
make: *** [Makefile:45: idris-commands.elc] Error 1
Error: Process completed with exit code 2.

I wonder if file-name-parent-directory is new for 29.X and we need to be backwards compatible for 27.X and 28.X. (Comparing this and this) shows me that the function is missing)

[keram]

I wonder if file-name-parent-directory is new for 29.X and we need to be backwards compatible for 27.X and 28.X.

Yes, I think we can backport it into ./idris-compat.el . Will update this pull request later this week.
I was curious if the pipeline will pass on first try and to catch something like this.
Thanks for looking to the draft already ! :)

[jfdm]

Is this good to go now?

[keram]

Yes I think so.
I havent work with Idris for some time so did quick test now.
Loaded few random files in the Idris2 repository itself and everythink worked well on this branch. 🆗