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

F* can't find one enum constructor after it found an isomorphic one #3485

Open
briangmilnes opened this issue Sep 16, 2024 · 4 comments
Open

Comments

@briangmilnes
Copy link
Contributor

/// BUG F* can't find Three either as WrapOCaml.Three or Three !!
/// This works above for enum One which is only trivially different.
/// It works in language server but not with either a recent
/// dev release or an opam development release.
/// The OCaml is not required for this bug.
/// F* 2024.08.14~dev
/// platform=Linux_x86_64
/// compiler=OCaml 4.14.2
/// date=2024-09-02 15:23:16 -0700
/// commit=445f713ad8b276864ba7e205e028813e19324b66

Compile line from Forge make:
/// /home/milnes/.opam/default/bin/fstar.exe --warn_error "-321-333-331" --use_hints --use_hint_hashes --record_hints --hint_dir _build/fstar/fst/hints --print_universes --print_implicits --cache_checked_modules --cache_dir _build/fstar/fst/checked --include src --include src/fstar/ --include src/fstar/fst/ --include /home/milnes/.opam/default/lib/fstar src/fstar/fst/Main.fst

See Main.fst line 132.
Main.txt
WrapOCaml.txt

The compilation in Forge is not needed to test this.

@briangmilnes
Copy link
Contributor Author

Oops old bug line in Main.fst. My issue on another function. Here is a clean Main.fst.
Main.txt

@briangmilnes
Copy link
Contributor Author

Closed, it's a bug in the way I'm calling depend in Forge, it is picking up a file from ../src!

@briangmilnes
Copy link
Contributor Author

Looking at this in more detail, I had an .fsti in X above X/src. And the include order found it first and does no duplicate detection on the includes. Which is totally appropriate. I'll change Forge to ignore files in X.

@briangmilnes
Copy link
Contributor Author

closed, thought I had.

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

No branches or pull requests

1 participant