Skip to content

Conversation

@giltho
Copy link
Contributor

@giltho giltho commented Dec 15, 2025

I want to use the dune "package management" (which is kind of a replacement for using opam separately). So far, it fails, and it seems to be because of this issue, where dune has issues dealing with symlinks.

This PR updates charon to avoid requiring a symlink for the tests, and uses dune's copy_files instead

@giltho giltho changed the title Use copy_files instead of symlink so for dune to be happy Use copy_files instead of symlink for dune to be happy Dec 15, 2025
Comment on lines -75 to -79
preCheck =
if doCheck then ''
ln -sf ${charon}/tests-llbc charon-ml/tests/test-outputs
'' else
"";
Copy link
Member

@Nadrieril Nadrieril Dec 15, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Something like this is needed because in the nix env the test outputs are otherwise not accessible

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You cuold rm -r test-outputs first, that should work

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, not sure what that means
Why does it need to be available for nix? Isn't dune taking care of all of this?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In nix we build the rust side and ocaml sides separately. So when we get to building the ocaml side, the llbc files emitted by running the rust tests are not there. We must put them there ourselves, which is what this does.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Anyway I can do the nix bits, but I'm not sure I want two copies to happen on the ocaml side

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aaaaah, got it
Closing this anyway until it works one the dune side

Signed-off-by: Sacha Ayoun <[email protected]>
(lib.hasPrefix (toString ../charon-ml) path)
|| (lib.hasPrefix (toString ../dune-project) path);
|| (lib.hasPrefix (toString ../dune-project) path)
|| (lib.hasPrefix (toString ../charon/tests/ui) path);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's not needed: ocaml only needs .llbc files, none of which are part of the git repo.

@giltho
Copy link
Contributor Author

giltho commented Dec 16, 2025

This still doesn't allow me to use dune package management so closing this for now until it's useful

@giltho giltho closed this Dec 16, 2025
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