project-everest
can't build evercddl on macos (Docker or native)
I tried a clean install on macOS 15.5 both natively and via Docker. FStar is clearly not getting installed correctly in either case.
Docker
I ran:
% git clone [email protected]:project-everest/everparse.git
% cd everparse
% docker build -t evercddl .
Step 8 fails:
=> ERROR [8/8] RUN sudo apt-get update && . "/home/opam/.cargo/env" && e 1.1s
------
> [8/8] RUN sudo apt-get update && . "/home/opam/.cargo/env" && env OPAMYES=1 make _opam && eval $(opam env) && make -j 24 -C opt && env OTHERFLAGS='--admit_smt_queries true' make -j 24 cbor-test cddl-test cose-test:
0.423 Hit:1 http://ports.ubuntu.com/ubuntu-ports noble InRelease
0.463 Get:2 http://ports.ubuntu.com/ubuntu-ports noble-updates InRelease [126 kB]
0.609 Hit:3 http://ports.ubuntu.com/ubuntu-ports noble-backports InRelease
0.657 Hit:4 http://ports.ubuntu.com/ubuntu-ports noble-security InRelease
0.679 Fetched 126 kB in 1s (218 kB/s)
0.679 Reading package lists...
1.039 make: '_opam' is up to date.
1.045 make: Entering directory '/mnt/everparse/opt'
1.045 make -C FStar ADMIT=1
1.045 make[1]: Entering directory '/mnt/everparse/opt/FStar'
1.048 EXTRACT STAGE 1 FSTARC-BARE
1.049 make[2]: Entering directory '/mnt/everparse/opt/FStar'
1.059 make[2]: *** No rule to make target '/Users/rohan/src/ietf/project-everest/everparse/opt/FStar/stage0/out/lib/fstar/ulib/FStar.Pervasives.fst', needed by '/Users/rohan/src/ietf/project-everest/everparse/opt/FStar/stage1/fstarc.checked/FStar.Pervasives.fst.checked.lax'. Stop.
1.059 make[2]: Leaving directory '/mnt/everparse/opt/FStar'
1.059 make[1]: Leaving directory '/mnt/everparse/opt/FStar'
1.059 make[1]: *** [Makefile:92: .bare1.src.touch] Error 2
1.059 make: *** [Makefile:31: FStar.do] Error 2
1.059 make: Leaving directory '/mnt/everparse/opt'
------
Dockerfile:27
--------------------
25 | # Build and publish the release
26 | ARG CI_THREADS=24
27 | >>> RUN sudo apt-get update && . "$HOME/.cargo/env" && env OPAMYES=1 make _opam && eval $(opam env) && make -j $CI_THREADS -C opt && env OTHERFLAGS='--admit_smt_queries true' make -j $CI_THREADS cbor-test cddl-test cose-test
28 |
29 | ENTRYPOINT ["/mnt/everparse/opt/shell.sh", "--login", "-c"]
--------------------
ERROR: failed to solve: process "/bin/sh -c sudo apt-get update && . \"$HOME/.cargo/env\" && env OPAMYES=1 make _opam && eval $(opam env) && make -j $CI_THREADS -C opt && env OTHERFLAGS='--admit_smt_queries true' make -j $CI_THREADS cbor-test cddl-test cose-test" did not complete successfully: exit code: 2
Natively
I ran:
% git clone [email protected]:project-everest/everparse.git
% cd everparse
% rustup component add rustfmt && cargo install bindgen-cli
% brew install opam bash gnu-getopt make
% ./build-evercddl.sh
I error out here:
+ make _opam
/Users/rohan/src/ietf/project-everest/everparse/src/common.Makefile:77: .depend: No such file or directory
true
/Users/rohan/src/ietf/project-everest/everparse/opt/FStar/out/bin/fstar.exe --include /Users/rohan/src/ietf/project-everest/everparse/opt/karamel/krmllib --include /Users/rohan/src/ietf/project-everest/everparse/opt/karamel/krmllib/obj --include /Users/rohan/src/ietf/project-everest/everparse/opt/pulse/out/lib/pulse --include src/lowparse --include src/ASN1 --include src/3d/prelude --include src/cbor/spec --include src/cbor/spec/raw --include src/cbor/spec/raw/everparse --include src/cddl/spec --include src/lowparse/pulse --include src/cbor/pulse --include src/cbor/pulse/raw --include src/cbor/pulse/raw/everparse --include src/cddl/pulse --include src/cddl/tool --include . --cache_checked_modules --warn_error @241 --already_cached PulseCore,Pulse,C,LowStar,*,-LowParse,-EverParse3d,-ASN1,-CBOR,-CDDL,Prims,FStar,LowStar --cmi --ext context_pruning --dep full @.depend.rsp --output_deps_to .depend.aux
* Warning 152:
- Not a valid include directory:
/Users/rohan/src/ietf/project-everest/everparse/opt/karamel/krmllib/obj
* Warning 152:
- Not a valid include directory:
/Users/rohan/src/ietf/project-everest/everparse/opt/pulse/out/lib/pulse
* Error 168 at src/lowparse/pulse/LowParse.Pulse.Base.fst(2,11-2,11):
- Unknown language extension pulse
1 error was reported (see above)
make: *** [.depend] Error 1
/Users/rohan/src/ietf/project-everest/everparse/opt/karamel/krmllib/ does not contain an obj directory and /Users/rohan/src/ietf/project-everest/everparse/opt/pulse/ does not contain an out directory.
Thanks Rohan for reporting!
- was due to a missing
git clean -ffdxin our Dockerfile. - was due to our assumed use of GNU Make and GCC.
I just merged #215, which I claim to solve those 2 issues. Could you please check again whether both scenarios now work for you? Thanks again!
Hi, On docker, I am getting the following:
967.1 * Error 17 at Spec.Loops.fst(5,0-11,30):
967.1 - Z3 solver not found.
967.1 - Required version: 4.8.5
967.1 - Please download version 4.8.5 of Z3 from
967.1 https://github.com/Z3Prover/z3/releases
967.1 and install it into your $PATH as 'z3-4.8.5'.
967.1 - Version 4.8.5 of Z3 should be included in binary packages of F*. If you are
967.1 using a binary package and are seeing this error, please file a bug report.
967.1
Note that earlier in the run I see the following:
955.1 mkdir -p z3
955.1 FStar/.scripts/get_fstar_z3.sh /mnt/everparse/opt/z3
955.1 >>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version. You need to install qemu-user (and shared libraries) to execute it.
955.1 >>> Downloading Z3 4.8.5 from https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip ...
957.1 >>> Installed Z3 4.8.5 to /mnt/everparse/opt/z3/z3-4.8.5
957.1 >>> Downloading Z3 4.13.3 from https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-glibc-2.34.zip ...
960.1 >>> Installed Z3 4.13.3 to /mnt/everparse/opt/z3/z3-4.13.3
Note that Z3 release 4.13.3 was on Oct 11, 2024 and release 4.8.5 was on Jun 3, 2019 (over 6 years old). Maybe Spec.Loops.fst using a more recent release would be nice.
Regarding building natively, ./build-evercddl.sh completes with the following line, but I cannot find cddl.exe anywhere.
gmake: Leaving directory '/Users/rohan/src/ietf/project-everest/everparse/opt'
Hi, On docker, I am getting the following:
967.1 * Error 17 at Spec.Loops.fst(5,0-11,30): 967.1 - Z3 solver not found. 967.1 - Required version: 4.8.5Note that Z3 release 4.13.3 was on Oct 11, 2024 and release 4.8.5 was on Jun 3, 2019 (over 6 years old). Maybe Spec.Loops.fst using a more recent release would be nice.
Use of Z3 4.8.5 in F* projects is a long-standing issue, and the process of migrating to 4.13.3 is nearing completion, see FStarLang/FStar#3880 . One main reason for this upcoming migration is indeed the inability to build Z3 4.8.5 on Apple Silicon, so yes, we are well aware of this issue, and we are actively working on it, we should be done hopefully in the next few weeks.
Until this happens, could you please try with enabling Rosetta on the host and running docker build --platform linux/amd64 , following https://stackoverflow.com/q/75912343 ? Thanks again!
Regarding building natively,
./build-evercddl.shcompletes with the following line, but I cannot findcddl.exeanywhere.gmake: Leaving directory '/Users/rohan/src/ietf/project-everest/everparse/opt'
This indicates that building EverParse dependencies failed, and after looking up on my side, this is the same error as the one you have with Docker, due to Z3 4.8.5. Could you please try with Rosetta enabled? Thanks again!
Hi @rohanmahy . We have improved support for MacOS, and we have revised the build system of EverParse and EverCDDL. Can you please try again following the instructions from README.md? Thanks in advance!