search

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
395 stars 59 forks source link

Trouble compiling Kremlin on osx #113

Closed ptrcmd closed 6 years ago

ptrcmd commented 6 years ago

I am using OSX 10.13 High Sierra with ocaml 4.06.1. I cloned and built fstar git master, and I got the following error when I executed make: 

$ make
ocamlbuild -I src -I lib -I parser -I kremlib -use-menhir -use-ocamlfind -classic-display -menhir "menhir --infer --explain" Kremlin.native Tests.native
ln -sf Kremlin.native krml
Didn't find fstarlib via ocamlfind or in FSTAR_HOME (which is: ); run make -C /ulib/ml
make: *** [pre] Error 1

I have fstar.exe in PATH, and I already executed make under ulib/ml under where I cloned FStar. After setting FSTAR_HOME to where I cloned FStar, I got the following error:

$ make
ocamlbuild -I src -I lib -I parser -I kremlib -use-menhir -use-ocamlfind -classic-display -menhir "menhir --infer --explain" Kremlin.native Tests.native
ln -sf Kremlin.native krml
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C kremlib
../krml -fparentheses -fcurly-braces -fno-shadow -minimal -tmpdir extracted -warn-error +9+11 -skip-compilation -extract-uints \
      -add-include '<inttypes.h>' -add-include '"kremlib.h"' -add-include '"kremlin/internal/compat.h"' \

KreMLin: from a ML-like subset to C

Usage: ../krml [OPTIONS] FILES

High-level description:
  1. If some FILES end with .fst or .fsti, and [-verify] is set, KreMLin will
     call [fstar] on them to perform verification.
  2. If some FILES end with .fst or .fsti, KreMLin will call [fstar] on them to
     perform extraction and produce [out.krml].
  3. If exactly one FILE ends with [.krml] or [.json], or if a [.krml] file was
     produced at step 2., KreMLin will generate a series of [.c] and [.h] files
     in the directory specified by [-tmpdir], or in the current directory.
  4. If some FILES end with [.c], KreMLin will compile them along with the [.c]
     files generated at step 3. to obtain a series of [.o] files.
  5. If some FILES end with [.o], [.S] or [.a], KreMLin will link them along with the
     [.o] files obtained at step 4. to obtain a final executable.

The [-skip-extraction] option stops KreMLin after step 1.
The [-skip-translation] option stops KreMLin after step 2.
The [-skip-compilation] option stops KreMLin after step 3.
The [-skip-linking] option stops KreMLin after step 4.

The [-warn-error] option follows the OCaml syntax, namely:
  - [r] is a range of warnings (either a number [n], or a range [n..n])
  - [-r] silences range [r]
  - [+r] enables range [r]
  - [@r] makes range [r] fatal.

The default is +1..2@3+4..8@9+10@11+12..16 and the available warnings are:
  1: not generating code for a provided file
  2: found a reference to a function without implementation
  3: external command failed
  4: type error / malformed input
  5: type definition contains an application of an undefined type abbreviation
  6: variable-length array
  7: private F* function cannot be marked as C static
  8: C inline function reference across translation units
  9: need to manually call static initializers for globals
  10: deprecated feature
  11: subexpression is not Low*; cannot proceed
  12: cannot be compiled to Wasm
  13: monomorphic instance about to be dropped
  14: cannot perform tail-call optimization
  15: function is not Low*; need compatibility headers

The [-bundle] option takes an argument of the form Api=Pattern1,...,Patternn
The Api= part is optional and Api is made up of a non-empty list of modules
separated by + (for instance: Interface1+Interface2). A pattern is either Foo.Bar
(exact match) or Foo.Baz.* (prefix). The semantics are as follows: all the
modules that match a pattern are grouped into a single C translation unit, and
their declarations are marked as static, inasmuch as cross-translation unit
calls permit. If the Api= part is present, then the module named Api must be
found within the set of input files, and its declarations are appended to the
translation unit without any visibility modifications.

The default arguments are:

All include directories and paths supports special prefixes:
  - if a path starts with FSTAR_LIB, this will expand to wherever F*'s ulib
    directory is
  - if a path starts with FSTAR_HOME, this will expand to wherever the source
    checkout of F* is (this does not always exist, e.g. in the case of an OPAM
    setup)

The compiler switches turn on the following options.
  [-cc gcc] (default) adds [-ccopts -Wall,-Werror,-Wno-unused-variable,-Wno-unknown-warning-option,-Wno-unused-but-set-variable,-g,-fwrapv,-fstack-check,-D_BSD_SOURCE,-D_DEFAULT_SOURCE,-Wno-parentheses -ccopt -std=c11]
  [-cc clang] adds [-ccopts -Wall,-Werror,-Wno-unused-variable,-Wno-unknown-warning-option,-Wno-unused-but-set-variable,-g,-fwrapv,-fstack-check,-D_BSD_SOURCE,-D_DEFAULT_SOURCE,-Wno-parentheses -ccopt -std=c11]
  [-cc g++] adds [-ccopts -Wall,-Werror,-Wno-unused-variable,-Wno-unknown-warning-option,-Wno-unused-but-set-variable,-g,-fwrapv,-fstack-check,-D_BSD_SOURCE,-D_DEFAULT_SOURCE,-Wno-parentheses]
  [-cc msvc] adds [-warn-error +6 -falloca]
  [-cc compcert] adds [-warn-error @6@8 -fnostruct-passing -fnoanonymous-unions -ccopts -g,-D_BSD_SOURCE,-D_DEFAULT_SOURCE]

The [-fc89] option triggers [-fnoanonymous-unions], [-fnocompound-literals] and
[-fc89-scope]. It also changes the invocations above to use [-std=c89]. Note
that if you're using the uint128 type, you will have to manually compile this
code with -DKRML_VERIFIED_UINT128.

To debug Wasm codegen, it might be useful to trigger the same compilation path
as Wasm, but emit C code instead. This can be achieved with [-wasm -d
force-c,c-calls,wasm-calls -drop C,TestLib -add-include '"hack.h"']
where [hack.h] contains [#define WasmSupport_check_buffer_size(X)].

Supported options:
  -cc                     compiler to use; one of gcc (default), compcert, g++, clang, msvc
  -m32                    turn on 32-bit cross-compiling
  -fsopt                  option to pass to F* (use -fsopts to pass a comma-separated list of values)
  -ccopt                  option to pass to the C compiler and linker (use -ccopts to pass a comma-separated list of values)
  -ldopt                  option to pass to the C linker (use -ldopts to pass a comma-separated list of values)
  -skip-extraction        stop after step 1.
  -skip-translation       stop after step 2.
  -skip-compilation       stop after step 3.
  -skip-linking           stop after step 4.
  -verify                 ask F* to verify the program
  -verbose                show the output of intermediary tools when acting as a driver for F* or the C compiler
  -diagnostics            list recursive functions and overly nested data types (useful for MSVC)
  -wasm                   emit a .wasm file instead of C

  -add-early-include      prepend #include the-argument to every generated file, before kremlib.h
  -add-include            prepend #include the-argument to every generated file, after the #define __FOO_H
  -add-include-tmh        append #include <FILE.tmh>, where FILE is the current basename
  -minimal                do not prepend #include "kremlib.h"; do not bundle FStar
  -static-header          generate a .h for the given module where all functions are marked a static inline
  -no-prefix              don't prepend the module name to declarations from this module
  -bundle                 group modules into a single C translation unit (see above)
  -drop                   do not extract code for this module (see above)
  -library                this is a model and all functions should be made abstract
  -header                 prepend the contents of the given file at the beginning of each .c and .h
  -tmpdir                 temporary directory for .out, .c, .h and .o files
  -I                      add directory to search path (F* and C compiler)
  -o                      name of the resulting executable
  -warn-error             decide which errors are fatal / warnings / silent (default: +1..2@3+4..8@9+10@11+12..16)

  -by-ref                 pass the given struct type by reference, always
  -fbuiltin-uint128       target compiler supports arithmetic operators for uint128 -- this is NON PORTABLE, works only with GCC/Clang
  -falloca                use alloca(3) for variable-length arrays on the stack
  -fnostruct-passing      disable passing structures by value and use pointers instead
  -fnoanonymous-unions    disable C11 anonymous unions
  -fnocompound-literals   don't generate C11 compound literals
  -ftail-calls            statically compile tail-calls into loops
  -funroll-loops          textually expand loops smaller than N
  -fparentheses           add unnecessary parentheses to silence GCC and Clang's -Wparentheses
  -fno-shadow             add unnecessary renamings to defeat GCC and Clang's -Wshadow, as well as the various MSVC warnings
  -fcurly-braces          always add curly braces around blocks
  -fnoshort-enums         use C11 enums instead of C macros and uint8_t for enums
  -fc89-scope             use C89 scoping rules
  -fc89                   generate C89-compatible code (meta-option, see above)

  -djson                  dump the input AST as JSON
  -dast                   pretty-print the internal AST
  -dmonomorphization      pretty-print the internal AST after monomorphization
  -dinline                pretty-print the internal AST after inlining
  -dpattern               pretty-print after pattern matches compilation
  -dsimplify              pretty-print the internal AST after going to a statement language
  -dstructs               pretty-print the internal AST after struct transformations
  -dc                     pretty-print the output C
  -dwasm                  pretty-print the output Wasm
  -d                      debug the specific comma-separated list of values; currently supported: inline,bundle,reachability,c-calls,wasm-calls,wasm-memory,wasm,force-c,cflat

  -help                   Display this list of options
  --help                  Display this list of options

make[1]: *** [extracted/Makefile.include] Error 1
make: *** [kremlib] Error 2
msprotz commented 6 years ago

Hello,

Thanks for reporting the issue. Some things to try out:

Thanks,

Jonathan

msprotz commented 6 years ago

note that recent versions of gnu make can be obtained via homebrew and oftentimes are available via the alias gmake

ptrcmd commented 6 years ago

Hi,

I installed GNU make 4.2.1 via brew, and running gmake worked! Thanks!

ptrcmd commented 6 years ago

Perhaps this should be on the installation guide (README.md) for osx?

msprotz commented 6 years ago

Done, thanks for the suggestion!