everest icon indicating copy to clipboard operation
everest copied to clipboard

Build Fstar fails when using ./everest make.

Open kgardas opened this issue 3 years ago • 1 comments

Hello, following instructions and recommendations from ./everest check I've installed everything as needed and allowed ./everst script to do whatever it needed to do. Anyway, the build, e.g. ./everest make step fails with:

$ ./everest make
# Switching to the everest directory ... now in /home/karel/vcs/everest

exported FSTAR_HOME=/home/karel/vcs/everest/FStar
exported OPENSSL_HOME=/home/karel/vcs/everest/MLCrypto/openssl
exported KREMLIN_HOME=/home/karel/vcs/everest/kremlin
exported VALE_HOME=/home/karel/vcs/everest/vale
exported HACL_HOME=/home/karel/vcs/everest/hacl-star
exported MLCRYPTO_HOME=/home/karel/vcs/everest/MLCrypto
exported LD_LIBRARY_PATH=/home/karel/vcs/everest/MLCrypto/openssl:
exported PATH=/home/karel/vcs/everest/FStar/bin:/home/karel/vcs/everest/kremlin:/home/karel/vcs/everest/z3-4.8.5-x64-ubuntu-14.04/bin:/home/karel/vcs/everest/z3-4.8.5-x64-ubuntu-14.04/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin:/home/karel/vcs/everest/FStar/bin:/home/karel/vcs/everest/kremlin
================================================================================
Rebuilding FStar
Running: build_fstar
make: Entering directory '/home/karel/vcs/everest/FStar/src/ocaml-output'
[MAKE FStar_Version.ml]
make -C ../../ulib/ml/ intfiles
make[1]: Entering directory '/home/karel/vcs/everest/FStar/ulib/ml'
make[1]: Nothing to be done for 'intfiles'.
make[1]: Leaving directory '/home/karel/vcs/everest/FStar/ulib/ml'
[OCAMLBUILD]
+ ocamlfind ocamldep -package stdint -package compiler-libs -package compiler-libs.common -package menhirLib -package dynlink -package pprint -package ulex -package yojson -package ocaml-migrate-parsetree -package process -package batteries -package zarith -package ppx_deriving.std -package ppx_deriving_yojson -modules src/fstar/ml/main.ml > src/fstar/ml/main.ml.depends
ocamlfind: Package `stdint' not found
Command exited with code 2.
Compilation unsuccessful after building 1 target (0 cached) in 00:00:00.
make: *** [Makefile:115: _build/src/fstar/ml/main.native] Error 10
make: Leaving directory '/home/karel/vcs/everest/FStar/src/ocaml-output'
================================================================================
FAILURE: build failed for FStar
karel@everest:~/vcs/everest$

This happens for two last weeks at least even if I allowed ./everest pull to pull the latest.

The platform is solely installed Ubuntu 20.04 LTS VM.

kgardas avatar Mar 03 '21 17:03 kgardas

When doing ./everest check, into which configuration file was the call to .opam/.../init.sh appended? Do you have more than one of .bash_profile, .profile, etc.?

tahina-pro avatar Mar 22 '21 20:03 tahina-pro