Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Build Fstar fails when using ./everest make. #81

Open
kgardas opened this issue Mar 3, 2021 · 1 comment
Open

Build Fstar fails when using ./everest make. #81

kgardas opened this issue Mar 3, 2021 · 1 comment

Comments

@kgardas
Copy link

kgardas commented Mar 3, 2021

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.

@tahina-pro
Copy link
Member

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.?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants