nix: bootstrap is broken

FStarLang / FStar

A Proof-oriented Programming Language

https://fstar-lang.org

Apache License 2.0

2.68k stars 232 forks source link

nix: bootstrap is broken #3181

Open pnmadelaine opened 9 months ago

pnmadelaine commented 9 months ago

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)

mtzguido commented 9 months ago

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?