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

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

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

keram
Copy link
Contributor

@keram keram commented Jul 8, 2024

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
Copy link
Contributor

jfdm commented Jul 9, 2024

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
Copy link
Contributor

jfdm commented Jul 9, 2024

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
Copy link
Contributor Author

keram commented Jul 9, 2024

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 ! :)

"source dir" and "relative file path" or
"work dir" and "relative file path" when idris protocol version
is greater than 1.

Why:
In Idris2 the files are loaded relative to work directory
which is a directory containing an ".ipkg" file.

Relates to:
idris-lang/Idris2#3310
idris-hackers#627
@keram keram force-pushed the idris-filename-to-load-v2 branch from 51e59b6 to 92b7e1b Compare July 15, 2024 13:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants