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

[ fix ] Only set IDRIS2_PREFIX if it is unset (fixes Issue 3022) #3024

Merged
merged 4 commits into from
Jul 31, 2023

Conversation

CodingCellist
Copy link
Collaborator

Description

Discovered by scarf005 in #3022, if the IDRIS2_PREFIX envvar is set, bootstrapping fails. This happens regardless of PREFIX being set or not, and only happens if IDRIS2_PREFIX is set.

Changing the syntax in the Makefile to use ?= (assign-if-unset) instead of := (assign) seems to fix the issue.

I also updated the envvars.rst docs, because they were outdated and didn't mention PREFIX being a thing (something which could've avoided the issue, but also would've left it buried for someone else to unearth). There were several changes, e.g. #2649, which weren't included.

Should this change go in the CHANGELOG?

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG.md (and potentially also
    CONTRIBUTORS.md).

Original issue spotted and reported by scarf005 and Stefan Höck.

For some reason, using `:=` instead of `?=` in the Makefile causes the
second part of bootstrapping to fail. So the fix is to use `?=`.

Fixes idris-lang#3022
We've modified the environment variables, but nobody seemingly bothered
updating the docs.

Discovered as part of idris-lang#3022
As well as the envvars doc update.
@dunhamsteve
Copy link
Contributor

Previously envvars.rst described the environment variables consulted by Idris at runtime, and PREFIX is only used by the Makefile. Should we list build-time environment variables separately?

@CodingCellist
Copy link
Collaborator Author

Previously envvars.rst described the environment variables consulted by Idris at runtime, and PREFIX is only used by the Makefile. Should we list build-time environment variables separately?

Probably sensible. On the same page, but under different subheadings?

@gallais gallais merged commit 51403ab into idris-lang:main Jul 31, 2023
20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
admin: installation documentation Improvements or additions to documentation enhancement
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Bootstrapped Idris2 fails to resolve paths when IDRIS2_PREFIX is manually set
3 participants