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

Replace the 'dev-why3' binary by 'dev-env' which sets shell environment variables #986

Merged
merged 1 commit into from
Apr 5, 2024

Conversation

Armael
Copy link
Contributor

@Armael Armael commented Apr 5, 2024

This is strictly more flexible: instead of requiring the use of a custom why3 wrapper, we provide a way to setup a shell environment where why3 resolves to the correct binary, and WHY3CONFIG indicates the config file.

This should then "just work" for binaries such as why3_tools that link to the why3 api, since they will pick up WHY3CONFIG.

@xldenis it may be useful for you to test this to check that it works in presence of paths with spaces or other unexpected macos weirdness.
It should be enough to check that the output of cargo run --bin dev-env looks reasonable, and that eval $(cargo run --bin dev-env) updated PATH and WHY3CONFIG in a way that works. Alternatively you could also check that ./ide still works...

…nt variables

This is strictly more flexible: instead of requiring the use of a
custom why3 wrapper, we provide a way to setup a shell environment
where `why3` resolves to the correct binary, and WHY3CONFIG indicates
the config file.

This will then "just work" for binaries such as why3_tools that link
to the why3 api, since they will pick up WHY3CONFIG.
@Armael
Copy link
Contributor Author

Armael commented Apr 5, 2024

To be perhaps clearer: the motivation for this PR is that currently, there's no easy way to launch why3_tools so that it uses the why3 config produced by creusot setup. Instead there's a way to launch why3 -C path/to/the/config which is what the dev-why3 wrapper does, but it doesn't generalizes to why3_tools since that's a separate binary.
So instead of this why3 wrapper I propose to have a binary to setup the PATH and WHY3CONFIG environment variables, which works both to launch why3 and why3_tools.

@xldenis
Copy link
Collaborator

xldenis commented Apr 5, 2024

To be clear, this doesn't change the invocation of commands like cargo creusot why3 ide, right? it only offers an additional way to get a shell with the correct why3 available?

@xldenis
Copy link
Collaborator

xldenis commented Apr 5, 2024

I confirmed that ./ide works and that env was properly updated.

@Armael
Copy link
Contributor Author

Armael commented Apr 5, 2024

correct, it's just an extra mechanism to launch the correct why3, it doesn't change cargo creusot why3 ide

@xldenis xldenis merged commit 1357cc9 into creusot-rs:master Apr 5, 2024
4 checks passed
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