FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Published 20 hours ago • verified publisher icon FStarLang

nix: bootstrap is broken

Open pnmadelaine opened this issue 1 year ago • 1 comments

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)

pnmadelaine avatar Dec 22 '23 21:12 pnmadelaine

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?

mtzguido avatar Dec 23 '23 21:12 mtzguido