You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When trying to bootstrap F* using Nix, .#fstar-ocaml-snapshot fails to build, throwing the following error:
* Error 54 at /nix/store/4skgqa9fayjbaw5fklzp2prj5q27nag6-fstar-0806a005a879f256ff5af6736fbea4d45ea6f6ca/lib/fstar/prims.fst(477,30-477,31):
- a is not equal to the expected type b
- See also /nix/store/4skgqa9fayjbaw5fklzp2prj5q27nag6-fstar-0806a005a879f256ff5af6736fbea4d45ea6f6ca/lib/fstar/prims.fst(477,14-477,15)
The text was updated successfully, but these errors were encountered:
Hi @pnmadelaine. This error happens if F* tries to check prims.fst in --MLish --lax mode: prims contains heterogeneous equality which is not properly typed in a simply typed system (which is roughly what MLish implements). Our makefiles currently make sure to not pass --MLish to any file in ulib, and only use it on compiler files, at least they should : ).
I'm not very familiar with Nix yet : ). Do you know where the F* call is coming from? Is Nix calling into the Makefiles?
When trying to bootstrap F* using Nix,
.#fstar-ocaml-snapshot
fails to build, throwing the following error:The text was updated successfully, but these errors were encountered: