Comments (13)
KreMLin requires OCaml (>= 4.05.0, < 4.10.0)
$ opam switch create 4.05.0
$ opam switch
# switch compiler description
→ 4.05.0 ocaml-base-compiler.4.05.0 4.05.0
$ opam install ppx_deriving_yojson zarith pprint menhir sedlex process fix wasm.1.0.1 visitors ctypes-foreign ctypes
--snip--
∗ installed wasm.1.0.1
[ERROR] The compilation of ocaml-secondary-compiler failed at "/home/kiwamu/.opam/opam-init/hooks/sandbox.sh build make -j3 world.opt".
#=== ERROR while compiling ocaml-secondary-compiler.4.08.1-1 ==================#
# context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://opam.ocaml.org#fc695fe5
# path ~/.opam/4.05.0/.opam-switch/build/ocaml-secondary-compiler.4.08.1-1
# command ~/.opam/opam-init/hooks/sandbox.sh build make -j3 world.opt
# exit-code 2
# env-file ~/.opam/log/ocaml-secondary-compiler-35975-14c197.env
# output-file ~/.opam/log/ocaml-secondary-compiler-35975-14c197.out
### output ###
# [...]
# echo '#!' | tr -d '\012' > camlheader_ur;
# ../boot/ocamlrun ../boot/ocamlc -use-prims ../runtime/primitives -strict-sequence -absname -w +a-4-9-41-42-44-45-48 -g -warn-error A -bin-annot -nostdlib -safe-string -strict-formats -nopervasives -c camlinternalFormatBasics.ml
# ../boot/ocamlrun ../boot/ocamlc -use-prims ../runtime/primitives -strict-sequence -absname -w +a-4-9-41-42-44-45-48 -g -warn-error A -bin-annot -nostdlib -safe-string -strict-formats -nopervasives -no-alias-deps -w -49 -pp "$AWK -f expand_module_aliases.awk" -c stdlib.mli
# gawk: fatal: can't open source file `expand_module_aliases.awk' for reading (No such file or directory)
# File "/home/kiwamu/.opam/4.05.0/.opam-switch/build/ocaml-secondary-compiler.4.08.1-1/stdlib/stdlib.mli", line 1:
# Error: Error while running external preprocessor
# Command line: gawk -f expand_module_aliases.awk 'stdlib.mli' > /tmp/ocamlpp253857
#
# make[1]: *** [Makefile:251: stdlib.cmi] Error 2
# make[1]: *** Waiting for unfinished jobs....
# make[1]: Leaving directory '/home/kiwamu/.opam/4.05.0/.opam-switch/build/ocaml-secondary-compiler.4.08.1-1/stdlib'
# make: *** [Makefile:325: coldstart] Error 2
???
from postmortem.
On Debian Buster:
$ sudo apt install libgmp-dev pkg-config libffi-dev z3
$ opam install fstar
$ export FSTAR_HOME=$HOME/.opam/default/.opam-switch/sources/fstar.0.9.3.0-beta1
$ make -C $FSTAR_HOME/ulib/ml
$ opam install ppx_deriving_yojson zarith pprint menhir sedlex process fix wasm.1.0.1 visitors ctypes-foreign ctypes
$ git clone https://github.com/FStarLang/kremlin.git
$ cd kremlin
$ make
$ ./krml | head -1
KreMLin: from a ML-like subset to C
Umm...
from postmortem.
Ah, we should use Everest script.
from postmortem.
On Debian Buster:
$ ./everest z3 opam
$ ./everest pull FStar make kremlin make
--snip--
================================================================================
Rebuilding FStar
Running: build_fstar
make: Entering directory '/home/vagrant/src/everest/FStar/src/ocaml-output'
Makefile:79: *** Correct version of menhir not found (needs a version newer than 20161115). Stop.
make: Leaving directory '/home/vagrant/src/everest/FStar/src/ocaml-output'
================================================================================
FAILURE: build failed for FStar
$ opam install menhir
[NOTE] Package menhir is already installed (current version is 20200624).
???
from postmortem.
Firstly we should read documents instead of building the tool chain.
https://fstarlang.github.io/lowstar/html/Core.html
from postmortem.
Trying to use build_local.sh
...
from postmortem.
$ pwd
/home/kiwamu/src/everest
$ ./build_local.sh
--snip--
Step 29/29 : RUN rm .ssh/id_rsa
---> Running in 3d0a9ba1d49d
Removing intermediate container 3d0a9ba1d49d
---> ba91ed68ec19
Successfully built ba91ed68ec19
Successfully tagged everest:local
$ docker images|grep everest
everest local ba91ed68ec19 About a minute ago 12.9GB
projecteverest/everest-ci-linux 5edd5df537d4 d9d5e20936ac 24 hours ago 5.36GB
projecteverest/fstar-linux 0032bcd7fbb7 6472ab2a9a8a 5 weeks ago 8.85GB
from postmortem.
$ docker run -it everest:local /bin/bash
everest@263bc0a5d971:~$ cd ~/everest/kremlin/
everest@263bc0a5d971:~/everest/kremlin$ ./krml | head -3
KreMLin: from a ML-like subset to C
Usage: ./Kremlin.native [OPTIONS] FILES
from postmortem.
everest@263bc0a5d971:~$ eval $(opam env)
everest@263bc0a5d971:~$ export PATH=~/everest/z3/bin:$PATH
everest@263bc0a5d971:~$ export FSTAR_HOME=~/everest/FStar
everest@263bc0a5d971:~$ export KREMLIN_HOME=~/everest/kremlin
everest@263bc0a5d971:~$ cd ~/everest/kremlin/test/
everest@263bc0a5d971:~/everest/kremlin$ make
everest@263bc0a5d971:~/everest/kremlin/test$ cd ../book/
everest@263bc0a5d971:~/everest/kremlin/book$ make html
--snip--
writing output... [100%] tutorial/specs/Spec.Test
Warning, treated as error:
/home/everest/everest/kremlin/book/Toy.rst:13:toctree contains reference to document 'tutorial/specs/Spec.Bignum' that doesn't have a title: no link will be generated
make: *** [Makefile:37: html] Error 2
Umm...
from postmortem.
everest@263bc0a5d971:~/src/practice-krml$ cat simple.krml
module Intro
module P = LowStar.Printf
module C = LowStar.Comment
module B = LowStar.Buffer
open FStar.HyperStack.ST
open LowStar.BufferOps
let main (): St Int32.t =
push_frame ();
let b: B.buffer UInt32.t = B.alloca 0ul 8ul in
b.(0ul) <- 255ul;
C.comment "Calls to printf are desugared via meta-programming";
let s = "from Low*!" in
P.(printf "Hello from %s\nbuffer contents: %xul\n"
s 8ul b done);
pop_frame ();
0l
everest@263bc0a5d971:~/src/practice-krml$ $KREMLIN_HOME/krml simple.krml
Fatal error: exception Failure("input_value: bad object")
???
from postmortem.
$ docker images|grep everest
everest local cefd03ba92cb 4 days ago 13.2GB
projecteverest/everest-ci-linux 32c49e325035 79fb46300371 5 days ago 5.38GB
projecteverest/everest-ci-linux 5edd5df537d4 d9d5e20936ac 2 months ago 5.36GB
projecteverest/fstar-linux 0032bcd7fbb7 6472ab2a9a8a 4 months ago 8.85GB
$ docker run -it everest:local /bin/bash
everest@c56edec11d3e:~$ eval $(opam env)
everest@c56edec11d3e:~$ export PATH=~/everest/z3/bin:$PATH
everest@c56edec11d3e:~$ export FSTAR_HOME=~/everest/FStar
everest@c56edec11d3e:~$ export KREMLIN_HOME=~/everest/kremlin
everest@c56edec11d3e:~$ cd ~/everest/kremlin/test/
everest@c56edec11d3e:~/everest/kremlin/test$ make
--snip--
All verification conditions discharged successfully
mkdir -p dist/
/home/everest/everest/kremlin/krml -tmpdir dist/ -skip-compilation \
obj/FStar_Pervasives_Native.krml obj/FStar_Pervasives.krml obj/FStar_Mul.krml obj/FStar_Squash.krml obj/FStar_Classical.krml obj/FStar_Preorder.krml obj/FStar_Calc.krml obj/FStar_StrongExcludedMiddle.krml obj/FStar_List_Tot_Base.krml obj/FStar_List_Tot_Properties.krml o
bj/FStar_List_Tot.krml obj/FStar_Seq_Base.krml obj/FStar_FunctionalExtensionality.krml obj/FStar_Seq_Properties.krml obj/FStar_Seq.krml obj/FStar_Math_Lib.krml obj/FStar_Math_Lemmas.krml obj/FStar_BitVector.krml obj/FStar_UInt.krml obj/FStar_UInt32.krml obj/FStar_Int.krml
obj/FStar_Int16.krml obj/FStar_Ghost.krml obj/FStar_ErasedLogic.krml obj/FStar_UInt64.krml obj/FStar_Monotonic_Witnessed.krml obj/FStar_Order.krml obj/FStar_Reflection_Const.krml obj/FStar_VConfig.krml obj/FStar_Reflection_Types.krml obj/FStar_Reflection_Data.krml obj/FS
tar_Reflection_Builtins.krml obj/FStar_Reflection_Derived.krml obj/FStar_Reflection_Derived_Lemmas.krml obj/FStar_Set.krml obj/FStar_PropositionalExtensionality.krml obj/FStar_PredicateExtensionality.krml obj/FStar_TSet.krml obj/FStar_Monotonic_Heap.krml obj/FStar_Heap.kr
ml obj/FStar_Map.krml obj/FStar_Monotonic_HyperHeap.krml obj/FStar_Monotonic_HyperStack.krml obj/FStar_HyperStack.krml obj/FStar_HyperStack_ST.krml obj/FStar_Universe.krml obj/FStar_GSet.krml obj/FStar_ModifiesGen.krml obj/FStar_Range.krml obj/FStar_Tactics_Common.krml ob
j/FStar_Tactics_Types.krml obj/FStar_Tactics_Result.krml obj/FStar_Tactics_Effect.krml obj/FStar_Tactics_Builtins.krml obj/FStar_Reflection.krml obj/FStar_Tactics_Print.krml obj/FStar_Tactics_SyntaxHelpers.krml obj/FStar_Tactics_Util.krml obj/FStar_Reflection_Formula.krml
obj/FStar_Tactics_Derived.krml obj/FStar_Tactics_Logic.krml obj/FStar_Tactics.krml obj/FStar_BigOps.krml obj/LowStar_Monotonic_Buffer.krml obj/LowStar_Buffer.krml obj/FStar_Exn.krml obj/FStar_ST.krml obj/FStar_All.krml obj/FStar_List.krml obj/FStar_Int64.krml obj/FStar_I
nt32.krml obj/FStar_Int8.krml obj/FStar_UInt16.krml obj/FStar_UInt8.krml obj/FStar_Char.krml obj/FStar_String.krml obj/LowStar_Printf.krml obj/C.krml obj/A_Base.krml obj/A_Combinators.krml obj/A_Top.krml obj/FStar_Int_Cast.krml obj/B.krml obj/D.krml \
-warn-error @4@5@18 \
-fparentheses \
-static-header A.Base \
-library A.* \
-bundle 'B=A.*,FStar.*,LowStar.*,Prims,C' \
-bundle 'D=A.*,FStar.*,LowStar.*,Prims,C' \
-bundle 'A.*[rename=A,rename-prefix]' \
-no-prefix B \
-minimal \
-add-include '"A.h"' \
-o B.exe
✔ [Monomorphization] ⏱️ 75ms
✔ [Inlining] ⏱️ 4ms
✔ [Pattern matches compilation] ⏱️ 5ms
Warning 7: : After inlining, D.main2 (going into D) calls C.exit_code (going into B) -- removing the static qualifier from C.exit_code
Warning 7: : After inlining, D.main2 (going into D) calls LowStar.Printf.print_u64 (going into B) -- removing the static qualifier from LowStar.Printf.print_u64
✔ [Structs + Simplify 2] ⏱️ 5ms
✔ [Drop] ⏱️ 4ms
✔ [AstToCStar] ⏱️ 3ms
✔ [CStarToC] ⏱️ <1ms
⚙ KreMLin auto-detecting tools. Here's what we found:
readlink is: readlink
KreMLin called via: /home/everest/everest/kremlin/krml
KreMLin home is: /home/everest/everest/kremlin
⚙ KreMLin will drive F*. Here's what we found:
read FSTAR_HOME via the environment
fstar is on branch master
fstar is: /home/everest/everest/FStar/bin/fstar.exe /home/everest/everest/kremlin/runtime/WasmSupport.fst /home/everest/everest/FStar/ulib/FStar.UInt128.fst --trace_error --cache_checked_modules --expose_interfaces --include /home/everest/everest/kremlin/kremlib --include /home/everest/everest/kremlin/include
✔ [PrettyPrinting] ⏱️ 6ms
KreMLin: wrote out .c files for B, D
KreMLin: wrote out .h files for B, D
! test -e dist/A.h
make -C dist/ -f Makefile.basic USER_CFLAGS=-I/home/everest/everest/kremlin/test/sepcomp/a/dist
make[3]: Entering directory '/home/everest/everest/kremlin/test/sepcomp/b/dist'
cc -I. -I /home/everest/everest/kremlin/include -I /home/everest/everest/kremlin/kremlib/dist/minimal -Wall -Wextra -Werror -std=c11 -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-infinite-recursion -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -fPIC -I/home/everest/everest/kremlin/test/sepcomp/a/dist -c -o B.o B.c
cc -I. -I /home/everest/everest/kremlin/include -I /home/everest/everest/kremlin/kremlib/dist/minimal -Wall -Wextra -Werror -std=c11 -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-infinite-recursion -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -fPIC -I/home/everest/everest/kremlin/test/sepcomp/a/dist -c -o D.o D.c
cc -I. -I /home/everest/everest/kremlin/include -I /home/everest/everest/kremlin/kremlib/dist/minimal -Wall -Wextra -Werror -std=c11 -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-parameter -Wno-infinite-recursion -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -fPIC -I/home/everest/everest/kremlin/test/sepcomp/a/dist -o B.exe B.o D.o /home/everest/everest/kremlin/kremlib/dist/generic/libkremlib.a
make[3]: Leaving directory '/home/everest/everest/kremlin/test/sepcomp/b/dist'
dist/B.exe
1729make[2]: Leaving directory '/home/everest/everest/kremlin/test/sepcomp/b'
make[1]: Leaving directory '/home/everest/everest/kremlin/test/sepcomp'
everest@c56edec11d3e:~/everest/kremlin/test$ cd ../book/
everest@c56edec11d3e:~/everest/kremlin/book$ make html
ocaml fst2rst.ml < tutorial/specs/Spec.Bignum.fst > tutorial/specs/Spec.Bignum.rst
ocaml fst2rst.ml < tutorial/specs/Spec.Test.fst > tutorial/specs/Spec.Test.rst
ocaml fst2rst.ml < tutorial/code/Impl.Bignum.fst > tutorial/code/Impl.Bignum.rst
ocaml fst2rst.ml < tutorial/code/Impl.Bignum.Lemmas.fst > tutorial/code/Impl.Bignum.Lemmas.rst
ocaml fst2rst.ml < RingBuffer.fst > RingBuffer.rst
ocaml fst2rst.ml < LinkedList4.fst > LinkedList4.rst
ocaml fst2rst.ml < tutorial/code/Impl.Bignum.Intrinsics.fsti > tutorial/code/Impl.Bignum.Intrinsics.rst
mkdir -p _static
Running Sphinx v1.7.2
making output directory...
loading pickled environment... not yet created
building [mo]: targets for 0 po files that are out of date
building [html]: targets for 22 source files that are out of date
updating environment: 22 added, 0 changed, 0 removed
reading sources... [100%] tutorial/specs/Spec.Test
looking for now-outdated files... none found
pickling environment... done
checking consistency... done
preparing documents... done
writing output... [100%] tutorial/specs/Spec.Test
generating indices... genindex
writing additional pages... search
copying static files... done
copying extra files... done
dumping search index in English (code: en) ... done
dumping object inventory... done
build succeeded.
The HTML pages are in _build/html.
from postmortem.
Where should I take simple example of krml file to be compiled?
from postmortem.
I think I should take the other people's advice for this issue, because it may be not suitable for kernel layer...
from postmortem.
Related Issues (20)
- Avoid FreeBSD-SA-20:05.if_oce_ioctl HOT 2
- Avoid FreeBSD-SA-20:06.if_ixl_ioctl HOT 2
- Avoid FreeBSD-SA-20:14.sctp HOT 3
- Avoid FreeBSD-SA-19:22.mbuf
- Avoid FreeBSD-SA-20:13.libalias
- Avoid FreeBSD-SA-20:02.ipsec
- Write postmortem for 50 of FreeBSD Kernel Security Advisory HOT 5
- Avoid FreeBSD-SA-20:24.ipv6 HOT 1
- Avoid FreeBSD-SA-19:14.freebsd32 HOT 1
- Avoid FreeBSD-SA-19:02.fd HOT 2
- Avoid FreeBSD-SA-18:04.vt
- Avoid FreeBSD-SA-17:10.kldstat HOT 1
- Define array of char in typedef HOT 3
- Write SPARK code to avoid some of bugs HOT 2
- Write Zig code to avoid some of bugs HOT 8
- Write Idris code to avoid some of bugs HOT 1
- Write Checked C code to avoid some of bugs HOT 14
- Write Frama-C code to avoid some of bugs HOT 1
- Write postmortem for FreeBSD PR with ATS2 HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from postmortem.