search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Installing F* from the source on Mac OS X #1237

Closed VincentCheval closed 5 years ago

VincentCheval commented 7 years ago

Hello,

I'm trying to install F* from the source on Mac OS X and I'm facing a problem during Step 2 when I run make ocaml -C src. I obtain the following error:

Warning: could not find "msbuild", trying (deprecated) "xbuild"

mkdir -p boot
/Applications/Xcode.app/Contents/Developer/usr/bin/make extract_all

Warning: could not find "msbuild", trying (deprecated) "xbuild"

mkdir -p boot
../bin/fstar-any.sh --hint_info --eager_inference --lax --MLish --no_location_info --odir ocaml-output --codegen OCaml --include ../ulib --include boot --include basic --include extraction --include format --include fsdoc --include fstar --include parser --include prettyprint --include reflection --include smtencoding --include syntax --include tactics --include tosyntax --include typechecker ../ulib/FStar.Tactics.Types.fsti tactics/FStar.Tactics.Types.fs tactics/FStar.Tactics.Basic.fs tactics/FStar.Tactics.Embedding.fs tactics/FStar.Tactics.Native.fs boot/FStar.Tactics.Interpreter.fst --extract_namespace FStar.Tactics --no_extract FStar.Tactics.Native
/Users/vincentcheval/Documents/Recherche/Outils/FStar/src/boot/FStar.Util.fsti(32,11-32,19): (Error) Identifier not found: [System.DateTime]
Module System does not belong to the list of modules in scope, namely FStar.BaseTypes, FStar.Char, FStar.Float, FStar.UInt8, FStar.Int8, FStar.Int16, FStar.UInt16, FStar.Int32, FStar.Int64, FStar.Int, FStar.UInt64, FStar.UInt32, FStar.UInt, FStar.BitVector, FStar.Math.Lemmas, FStar.Math.Lib, FStar.Seq, FStar.Seq.Properties, FStar.Seq.Base, FStar.List.Tot, FStar.List.Tot.Properties, FStar.List.Tot.Base, FStar.Mul, FStar.All, FStar.ST, FStar.Heap, FStar.Monotonic.Heap, FStar.TSet, FStar.PredicateExtensionality, FStar.PropositionalExtensionality, FStar.StrongExcludedMiddle, FStar.Preorder, FStar.Set, FStar.FunctionalExtensionality, FStar.Classical, FStar.Squash, FStar.Exn, FStar.Pervasives, FStar.Pervasives.Native, Prims
1 error was reported (see above)
make[1]: *** [extract_tactics] Error 1
make: *** [ocaml] Error 2

I have the latest Sierra version (freshly reinstalled). All the previous steps worked.

Thanks a lot

Best Vincent

s-zanella commented 7 years ago

You need Mono installed to compile the sources using the F# compiler. We maintain an OCaml snapshot in the repository, so you can alternatively just run 'make -C src/ocaml-output' if you have a working OPAM setup. Most of us compile F* this way. There are a few differences between an F#-compiled version and an OCaml-compiled one, you'd be better off using the latter.

-----Original Message----- From: "Vincent Cheval" notifications@github.com Sent: ‎14/‎09/‎2017 12:43 To: "FStarLang/FStar" FStar@noreply.github.com Cc: "Subscribed" subscribed@noreply.github.com Subject: [FStarLang/FStar] Installing F* from the source on Mac OS X (#1237)

Hello, I'm trying to install F* from the source on Mac OS X and I'm facing a problem during Step 2 when I run make ocaml -C src. I obtain the following error: Warning: could not find "msbuild", trying (deprecated) "xbuild"

mkdir -p boot /Applications/Xcode.app/Contents/Developer/usr/bin/make extract_all

Warning: could not find "msbuild", trying (deprecated) "xbuild"

mkdir -p boot ../bin/fstar-any.sh --hint_info --eager_inference --lax --MLish --no_location_info --odir ocaml-output --codegen OCaml --include ../ulib --include boot --include basic --include extraction --include format --include fsdoc --include fstar --include parser --include prettyprint --include reflection --include smtencoding --include syntax --include tactics --include tosyntax --include typechecker ../ulib/FStar.Tactics.Types.fsti tactics/FStar.Tactics.Types.fs tactics/FStar.Tactics.Basic.fs tactics/FStar.Tactics.Embedding.fs tactics/FStar.Tactics.Native.fs boot/FStar.Tactics.Interpreter.fst --extract_namespace FStar.Tactics --no_extract FStar.Tactics.Native /Users/vincentcheval/Documents/Recherche/Outils/FStar/src/boot/FStar.Util.fsti(32,11-32,19): (Error) Identifier not found: [System.DateTime] Module System does not belong to the list of modules in scope, namely FStar.BaseTypes, FStar.Char, FStar.Float, FStar.UInt8, FStar.Int8, FStar.Int16, FStar.UInt16, FStar.Int32, FStar.Int64, FStar.Int, FStar.UInt64, FStar.UInt32, FStar.UInt, FStar.BitVector, FStar.Math.Lemmas, FStar.Math.Lib, FStar.Seq, FStar.Seq.Properties, FStar.Seq.Base, FStar.List.Tot, FStar.List.Tot.Properties, FStar.List.Tot.Base, FStar.Mul, FStar.All, FStar.ST, FStar.Heap, FStar.Monotonic.Heap, FStar.TSet, FStar.PredicateExtensionality, FStar.PropositionalExtensionality, FStar.StrongExcludedMiddle, FStar.Preorder, FStar.Set, FStar.FunctionalExtensionality, FStar.Classical, FStar.Squash, FStar.Exn, FStar.Pervasives, FStar.Pervasives.Native, Prims 1 error was reported (see above) make[1]: [extract_tactics] Error 1 make: [ocaml] Error 2 I have the latest Sierra version (freshly reinstalled). All the previous steps worked. Thanks a lot Best Vincent — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

cpitclaudel commented 7 years ago

@VincentCheval, did you figure this out? From here, it looks like a sed problem. Do you have gsed on your machine?

VincentCheval commented 7 years ago

Hello,

It worked with the command 'make -C src/ocaml-output' that @s-zanella pointed out. To answer your question though, I do have gsed installed.

cpitclaudel commented 7 years ago

OK, thanks. I'd like to understand what happened here. It looks like the sed parts of the boot target didn't run properly. Could you maybe run make -d -C src ocaml and post the output?

VincentCheval commented 7 years ago

That was one long output 😊

Good luck reading !

GNU Make 3.81
Copyright (C) 2006  Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.

This program built for i386-apple-darwin11.3.0
Reading makefiles...
Reading makefile `Makefile'...
Reading makefile `gmake/z3.mk' (search path) (no ~ expansion)...
Reading makefile `gmake/fstar.mk' (search path) (no ~ expansion)...

Warning: could not find "msbuild", trying (deprecated) "xbuild"

Updating makefiles....
 Considering target file `gmake/fstar.mk'.
  Looking for an implicit rule for `gmake/fstar.mk'.
  No implicit rule found for `gmake/fstar.mk'.
  Finished prerequisites of target file `gmake/fstar.mk'.
 No need to remake target `gmake/fstar.mk'.
 Considering target file `gmake/z3.mk'.
  Looking for an implicit rule for `gmake/z3.mk'.
  No implicit rule found for `gmake/z3.mk'.
  Finished prerequisites of target file `gmake/z3.mk'.
 No need to remake target `gmake/z3.mk'.
 Considering target file `Makefile'.
  Looking for an implicit rule for `Makefile'.
  No implicit rule found for `Makefile'.
  Finished prerequisites of target file `Makefile'.
 No need to remake target `Makefile'.
Updating goal targets....
Considering target file `ocaml'.
 File `ocaml' does not exist.
  Considering target file `boot'.
   File `boot' does not exist.
    Considering target file `boot/FStar.Util.fsti'.
     Looking for an implicit rule for `boot/FStar.Util.fsti'.
     Trying pattern rule with stem `FStar.Util'.
     Trying implicit prerequisite `basic/boot/FStar.Util.fsi'.
     Trying rule prerequisite `boot_dir'.
     Found an implicit rule for `boot/FStar.Util.fsti'.
      Considering target file `basic/boot/FStar.Util.fsi'.
       Looking for an implicit rule for `basic/boot/FStar.Util.fsi'.
       No implicit rule found for `basic/boot/FStar.Util.fsi'.
       Finished prerequisites of target file `basic/boot/FStar.Util.fsi'.
      No need to remake target `basic/boot/FStar.Util.fsi'.
      Considering target file `boot_dir'.
       File `boot_dir' does not exist.
       Finished prerequisites of target file `boot_dir'.
      Must remake target `boot_dir'.
mkdir -p boot
Putting child 0x7fbae4601710 (boot_dir) PID 8537 on the chain.
Live child 0x7fbae4601710 (boot_dir) PID 8537 
Reaping winning child 0x7fbae4601710 PID 8537 
Removing child 0x7fbae4601710 PID 8537 from chain.
      Successfully remade target file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.Util.fsti'.
     Prerequisite `basic/boot/FStar.Util.fsi' is older than target `boot/FStar.Util.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.Util.fsti'.
    No need to remake target `boot/FStar.Util.fsti'.
    Considering target file `boot/FStar.List.fsti'.
     Looking for an implicit rule for `boot/FStar.List.fsti'.
     Trying pattern rule with stem `FStar.List'.
     Trying implicit prerequisite `basic/boot/FStar.List.fsi'.
     Trying rule prerequisite `boot_dir'.
     Found an implicit rule for `boot/FStar.List.fsti'.
      Considering target file `basic/boot/FStar.List.fsi'.
       Looking for an implicit rule for `basic/boot/FStar.List.fsi'.
       No implicit rule found for `basic/boot/FStar.List.fsi'.
       Finished prerequisites of target file `basic/boot/FStar.List.fsi'.
      No need to remake target `basic/boot/FStar.List.fsi'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.List.fsti'.
     Prerequisite `basic/boot/FStar.List.fsi' is older than target `boot/FStar.List.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.List.fsti'.
    No need to remake target `boot/FStar.List.fsti'.
    Considering target file `boot/FStar.Bytes.fsti'.
     Looking for an implicit rule for `boot/FStar.Bytes.fsti'.
     Trying pattern rule with stem `FStar.Bytes'.
     Trying implicit prerequisite `basic/boot/FStar.Bytes.fsi'.
     Trying rule prerequisite `boot_dir'.
     Found an implicit rule for `boot/FStar.Bytes.fsti'.
      Considering target file `basic/boot/FStar.Bytes.fsi'.
       Looking for an implicit rule for `basic/boot/FStar.Bytes.fsi'.
       No implicit rule found for `basic/boot/FStar.Bytes.fsi'.
       Finished prerequisites of target file `basic/boot/FStar.Bytes.fsi'.
      No need to remake target `basic/boot/FStar.Bytes.fsi'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.Bytes.fsti'.
     Prerequisite `basic/boot/FStar.Bytes.fsi' is older than target `boot/FStar.Bytes.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.Bytes.fsti'.
    No need to remake target `boot/FStar.Bytes.fsti'.
    Considering target file `boot/FStar.String.fsti'.
     Looking for an implicit rule for `boot/FStar.String.fsti'.
     Trying pattern rule with stem `FStar.String'.
     Trying implicit prerequisite `basic/boot/FStar.String.fsi'.
     Trying rule prerequisite `boot_dir'.
     Found an implicit rule for `boot/FStar.String.fsti'.
      Considering target file `basic/boot/FStar.String.fsi'.
       Looking for an implicit rule for `basic/boot/FStar.String.fsi'.
       No implicit rule found for `basic/boot/FStar.String.fsi'.
       Finished prerequisites of target file `basic/boot/FStar.String.fsi'.
      No need to remake target `basic/boot/FStar.String.fsi'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.String.fsti'.
     Prerequisite `basic/boot/FStar.String.fsi' is older than target `boot/FStar.String.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.String.fsti'.
    No need to remake target `boot/FStar.String.fsti'.
    Considering target file `boot/FStar.Range.fsti'.
     Looking for an implicit rule for `boot/FStar.Range.fsti'.
     Trying pattern rule with stem `FStar.Range'.
     Trying implicit prerequisite `basic/boot/FStar.Range.fsi'.
     Trying rule prerequisite `boot_dir'.
     Found an implicit rule for `boot/FStar.Range.fsti'.
      Considering target file `basic/boot/FStar.Range.fsi'.
       Looking for an implicit rule for `basic/boot/FStar.Range.fsi'.
       No implicit rule found for `basic/boot/FStar.Range.fsi'.
       Finished prerequisites of target file `basic/boot/FStar.Range.fsi'.
      No need to remake target `basic/boot/FStar.Range.fsi'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.Range.fsti'.
     Prerequisite `basic/boot/FStar.Range.fsi' is older than target `boot/FStar.Range.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.Range.fsti'.
    No need to remake target `boot/FStar.Range.fsti'.
    Considering target file `boot/FStar.Pprint.fsti'.
     Looking for an implicit rule for `boot/FStar.Pprint.fsti'.
     Trying pattern rule with stem `FStar.Pprint'.
     Trying implicit prerequisite `basic/boot/FStar.Pprint.fsi'.
     Trying pattern rule with stem `FStar.Pprint'.
     Trying implicit prerequisite `prettyprint/boot/FStar.Pprint.fsi'.
     Trying rule prerequisite `boot_dir'.
     Found an implicit rule for `boot/FStar.Pprint.fsti'.
      Considering target file `prettyprint/boot/FStar.Pprint.fsi'.
       Looking for an implicit rule for `prettyprint/boot/FStar.Pprint.fsi'.
       No implicit rule found for `prettyprint/boot/FStar.Pprint.fsi'.
       Finished prerequisites of target file `prettyprint/boot/FStar.Pprint.fsi'.
      No need to remake target `prettyprint/boot/FStar.Pprint.fsi'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.Pprint.fsti'.
     Prerequisite `prettyprint/boot/FStar.Pprint.fsi' is older than target `boot/FStar.Pprint.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.Pprint.fsti'.
    No need to remake target `boot/FStar.Pprint.fsti'.
    Considering target file `boot/FStar.Parser.Parse.fsti'.
      Considering target file `parser/boot/parse.fsi'.
       Looking for an implicit rule for `parser/boot/parse.fsi'.
       No implicit rule found for `parser/boot/parse.fsi'.
       Finished prerequisites of target file `parser/boot/parse.fsi'.
      No need to remake target `parser/boot/parse.fsi'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.Parser.Parse.fsti'.
     Prerequisite `parser/boot/parse.fsi' is older than target `boot/FStar.Parser.Parse.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.Parser.Parse.fsti'.
    No need to remake target `boot/FStar.Parser.Parse.fsti'.
    Considering target file `boot/FStar.Tactics.Interpreter.fst'.
      Considering target file `tactics/boot/FStar.Tactics.Interpreter.fs'.
       Looking for an implicit rule for `tactics/boot/FStar.Tactics.Interpreter.fs'.
       No implicit rule found for `tactics/boot/FStar.Tactics.Interpreter.fs'.
       Finished prerequisites of target file `tactics/boot/FStar.Tactics.Interpreter.fs'.
      No need to remake target `tactics/boot/FStar.Tactics.Interpreter.fs'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.Tactics.Interpreter.fst'.
     Prerequisite `tactics/boot/FStar.Tactics.Interpreter.fs' is older than target `boot/FStar.Tactics.Interpreter.fst'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.Tactics.Interpreter.fst'.
    No need to remake target `boot/FStar.Tactics.Interpreter.fst'.
    Considering target file `boot/FStar.Tactics.Interpreter.fsti'.
      Considering target file `tactics/boot/FStar.Tactics.Interpreter.fsi'.
       Looking for an implicit rule for `tactics/boot/FStar.Tactics.Interpreter.fsi'.
       No implicit rule found for `tactics/boot/FStar.Tactics.Interpreter.fsi'.
       Finished prerequisites of target file `tactics/boot/FStar.Tactics.Interpreter.fsi'.
      No need to remake target `tactics/boot/FStar.Tactics.Interpreter.fsi'.
      Pruning file `boot_dir'.
     Finished prerequisites of target file `boot/FStar.Tactics.Interpreter.fsti'.
     Prerequisite `tactics/boot/FStar.Tactics.Interpreter.fsi' is older than target `boot/FStar.Tactics.Interpreter.fsti'.
     Prerequisite `boot_dir' is order-only for target `boot/FStar.Tactics.Interpreter.fsti'.
    No need to remake target `boot/FStar.Tactics.Interpreter.fsti'.
   Finished prerequisites of target file `boot'.
  Must remake target `boot'.
  Successfully remade target file `boot'.
 Finished prerequisites of target file `ocaml'.
Must remake target `ocaml'.
/Applications/Xcode.app/Contents/Developer/usr/bin/make extract_all
Putting child 0x7fbae47007a0 (ocaml) PID 8538 on the chain.
Live child 0x7fbae47007a0 (ocaml) PID 8538 
GNU Make 3.81
Copyright (C) 2006  Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.

This program built for i386-apple-darwin11.3.0
Reading makefiles...
Reading makefile `Makefile'...
Reading makefile `gmake/z3.mk' (search path) (no ~ expansion)...
Reading makefile `gmake/fstar.mk' (search path) (no ~ expansion)...

Warning: could not find "msbuild", trying (deprecated) "xbuild"

Updating makefiles....
 Considering target file `gmake/fstar.mk'.
  Looking for an implicit rule for `gmake/fstar.mk'.
  No implicit rule found for `gmake/fstar.mk'.
  Finished prerequisites of target file `gmake/fstar.mk'.
 No need to remake target `gmake/fstar.mk'.
 Considering target file `gmake/z3.mk'.
  Looking for an implicit rule for `gmake/z3.mk'.
  No implicit rule found for `gmake/z3.mk'.
  Finished prerequisites of target file `gmake/z3.mk'.
 No need to remake target `gmake/z3.mk'.
 Considering target file `Makefile'.
  Looking for an implicit rule for `Makefile'.
  No implicit rule found for `Makefile'.
  Finished prerequisites of target file `Makefile'.
 No need to remake target `Makefile'.
Updating goal targets....
Considering target file `extract_all'.
 File `extract_all' does not exist.
 Looking for an implicit rule for `extract_all'.
 No implicit rule found for `extract_all'.
  Considering target file `extract_tactics'.
   File `extract_tactics' does not exist.
    Considering target file `boot'.
     File `boot' does not exist.
      Considering target file `boot/FStar.Util.fsti'.
       Looking for an implicit rule for `boot/FStar.Util.fsti'.
       Trying pattern rule with stem `FStar.Util'.
       Trying implicit prerequisite `basic/boot/FStar.Util.fsi'.
       Trying rule prerequisite `boot_dir'.
       Found an implicit rule for `boot/FStar.Util.fsti'.
        Considering target file `basic/boot/FStar.Util.fsi'.
         Looking for an implicit rule for `basic/boot/FStar.Util.fsi'.
         No implicit rule found for `basic/boot/FStar.Util.fsi'.
         Finished prerequisites of target file `basic/boot/FStar.Util.fsi'.
        No need to remake target `basic/boot/FStar.Util.fsi'.
        Considering target file `boot_dir'.
         File `boot_dir' does not exist.
         Finished prerequisites of target file `boot_dir'.
        Must remake target `boot_dir'.
mkdir -p boot
Putting child 0x7fa5bb5072e0 (boot_dir) PID 8547 on the chain.
Live child 0x7fa5bb5072e0 (boot_dir) PID 8547 
Reaping winning child 0x7fa5bb5072e0 PID 8547 
Removing child 0x7fa5bb5072e0 PID 8547 from chain.
        Successfully remade target file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.Util.fsti'.
       Prerequisite `basic/boot/FStar.Util.fsi' is older than target `boot/FStar.Util.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.Util.fsti'.
      No need to remake target `boot/FStar.Util.fsti'.
      Considering target file `boot/FStar.List.fsti'.
       Looking for an implicit rule for `boot/FStar.List.fsti'.
       Trying pattern rule with stem `FStar.List'.
       Trying implicit prerequisite `basic/boot/FStar.List.fsi'.
       Trying rule prerequisite `boot_dir'.
       Found an implicit rule for `boot/FStar.List.fsti'.
        Considering target file `basic/boot/FStar.List.fsi'.
         Looking for an implicit rule for `basic/boot/FStar.List.fsi'.
         No implicit rule found for `basic/boot/FStar.List.fsi'.
         Finished prerequisites of target file `basic/boot/FStar.List.fsi'.
        No need to remake target `basic/boot/FStar.List.fsi'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.List.fsti'.
       Prerequisite `basic/boot/FStar.List.fsi' is older than target `boot/FStar.List.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.List.fsti'.
      No need to remake target `boot/FStar.List.fsti'.
      Considering target file `boot/FStar.Bytes.fsti'.
       Looking for an implicit rule for `boot/FStar.Bytes.fsti'.
       Trying pattern rule with stem `FStar.Bytes'.
       Trying implicit prerequisite `basic/boot/FStar.Bytes.fsi'.
       Trying rule prerequisite `boot_dir'.
       Found an implicit rule for `boot/FStar.Bytes.fsti'.
        Considering target file `basic/boot/FStar.Bytes.fsi'.
         Looking for an implicit rule for `basic/boot/FStar.Bytes.fsi'.
         No implicit rule found for `basic/boot/FStar.Bytes.fsi'.
         Finished prerequisites of target file `basic/boot/FStar.Bytes.fsi'.
        No need to remake target `basic/boot/FStar.Bytes.fsi'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.Bytes.fsti'.
       Prerequisite `basic/boot/FStar.Bytes.fsi' is older than target `boot/FStar.Bytes.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.Bytes.fsti'.
      No need to remake target `boot/FStar.Bytes.fsti'.
      Considering target file `boot/FStar.String.fsti'.
       Looking for an implicit rule for `boot/FStar.String.fsti'.
       Trying pattern rule with stem `FStar.String'.
       Trying implicit prerequisite `basic/boot/FStar.String.fsi'.
       Trying rule prerequisite `boot_dir'.
       Found an implicit rule for `boot/FStar.String.fsti'.
        Considering target file `basic/boot/FStar.String.fsi'.
         Looking for an implicit rule for `basic/boot/FStar.String.fsi'.
         No implicit rule found for `basic/boot/FStar.String.fsi'.
         Finished prerequisites of target file `basic/boot/FStar.String.fsi'.
        No need to remake target `basic/boot/FStar.String.fsi'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.String.fsti'.
       Prerequisite `basic/boot/FStar.String.fsi' is older than target `boot/FStar.String.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.String.fsti'.
      No need to remake target `boot/FStar.String.fsti'.
      Considering target file `boot/FStar.Range.fsti'.
       Looking for an implicit rule for `boot/FStar.Range.fsti'.
       Trying pattern rule with stem `FStar.Range'.
       Trying implicit prerequisite `basic/boot/FStar.Range.fsi'.
       Trying rule prerequisite `boot_dir'.
       Found an implicit rule for `boot/FStar.Range.fsti'.
        Considering target file `basic/boot/FStar.Range.fsi'.
         Looking for an implicit rule for `basic/boot/FStar.Range.fsi'.
         No implicit rule found for `basic/boot/FStar.Range.fsi'.
         Finished prerequisites of target file `basic/boot/FStar.Range.fsi'.
        No need to remake target `basic/boot/FStar.Range.fsi'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.Range.fsti'.
       Prerequisite `basic/boot/FStar.Range.fsi' is older than target `boot/FStar.Range.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.Range.fsti'.
      No need to remake target `boot/FStar.Range.fsti'.
      Considering target file `boot/FStar.Pprint.fsti'.
       Looking for an implicit rule for `boot/FStar.Pprint.fsti'.
       Trying pattern rule with stem `FStar.Pprint'.
       Trying implicit prerequisite `basic/boot/FStar.Pprint.fsi'.
       Trying pattern rule with stem `FStar.Pprint'.
       Trying implicit prerequisite `prettyprint/boot/FStar.Pprint.fsi'.
       Trying rule prerequisite `boot_dir'.
       Found an implicit rule for `boot/FStar.Pprint.fsti'.
        Considering target file `prettyprint/boot/FStar.Pprint.fsi'.
         Looking for an implicit rule for `prettyprint/boot/FStar.Pprint.fsi'.
         No implicit rule found for `prettyprint/boot/FStar.Pprint.fsi'.
         Finished prerequisites of target file `prettyprint/boot/FStar.Pprint.fsi'.
        No need to remake target `prettyprint/boot/FStar.Pprint.fsi'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.Pprint.fsti'.
       Prerequisite `prettyprint/boot/FStar.Pprint.fsi' is older than target `boot/FStar.Pprint.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.Pprint.fsti'.
      No need to remake target `boot/FStar.Pprint.fsti'.
      Considering target file `boot/FStar.Parser.Parse.fsti'.
        Considering target file `parser/boot/parse.fsi'.
         Looking for an implicit rule for `parser/boot/parse.fsi'.
         No implicit rule found for `parser/boot/parse.fsi'.
         Finished prerequisites of target file `parser/boot/parse.fsi'.
        No need to remake target `parser/boot/parse.fsi'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.Parser.Parse.fsti'.
       Prerequisite `parser/boot/parse.fsi' is older than target `boot/FStar.Parser.Parse.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.Parser.Parse.fsti'.
      No need to remake target `boot/FStar.Parser.Parse.fsti'.
      Considering target file `boot/FStar.Tactics.Interpreter.fst'.
        Considering target file `tactics/boot/FStar.Tactics.Interpreter.fs'.
         Looking for an implicit rule for `tactics/boot/FStar.Tactics.Interpreter.fs'.
         No implicit rule found for `tactics/boot/FStar.Tactics.Interpreter.fs'.
         Finished prerequisites of target file `tactics/boot/FStar.Tactics.Interpreter.fs'.
        No need to remake target `tactics/boot/FStar.Tactics.Interpreter.fs'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.Tactics.Interpreter.fst'.
       Prerequisite `tactics/boot/FStar.Tactics.Interpreter.fs' is older than target `boot/FStar.Tactics.Interpreter.fst'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.Tactics.Interpreter.fst'.
      No need to remake target `boot/FStar.Tactics.Interpreter.fst'.
      Considering target file `boot/FStar.Tactics.Interpreter.fsti'.
        Considering target file `tactics/boot/FStar.Tactics.Interpreter.fsi'.
         Looking for an implicit rule for `tactics/boot/FStar.Tactics.Interpreter.fsi'.
         No implicit rule found for `tactics/boot/FStar.Tactics.Interpreter.fsi'.
         Finished prerequisites of target file `tactics/boot/FStar.Tactics.Interpreter.fsi'.
        No need to remake target `tactics/boot/FStar.Tactics.Interpreter.fsi'.
        Pruning file `boot_dir'.
       Finished prerequisites of target file `boot/FStar.Tactics.Interpreter.fsti'.
       Prerequisite `tactics/boot/FStar.Tactics.Interpreter.fsi' is older than target `boot/FStar.Tactics.Interpreter.fsti'.
       Prerequisite `boot_dir' is order-only for target `boot/FStar.Tactics.Interpreter.fsti'.
      No need to remake target `boot/FStar.Tactics.Interpreter.fsti'.
     Finished prerequisites of target file `boot'.
    Must remake target `boot'.
    Successfully remade target file `boot'.
    Considering target file `../ulib/FStar.Tactics.Types.fsti'.
     Looking for an implicit rule for `../ulib/FStar.Tactics.Types.fsti'.
     No implicit rule found for `../ulib/FStar.Tactics.Types.fsti'.
     Finished prerequisites of target file `../ulib/FStar.Tactics.Types.fsti'.
    No need to remake target `../ulib/FStar.Tactics.Types.fsti'.
    Considering target file `tactics/FStar.Tactics.Types.fs'.
     Looking for an implicit rule for `tactics/FStar.Tactics.Types.fs'.
     No implicit rule found for `tactics/FStar.Tactics.Types.fs'.
     Finished prerequisites of target file `tactics/FStar.Tactics.Types.fs'.
    No need to remake target `tactics/FStar.Tactics.Types.fs'.
    Considering target file `tactics/FStar.Tactics.Basic.fs'.
     Looking for an implicit rule for `tactics/FStar.Tactics.Basic.fs'.
     No implicit rule found for `tactics/FStar.Tactics.Basic.fs'.
     Finished prerequisites of target file `tactics/FStar.Tactics.Basic.fs'.
    No need to remake target `tactics/FStar.Tactics.Basic.fs'.
    Considering target file `tactics/FStar.Tactics.Embedding.fs'.
     Looking for an implicit rule for `tactics/FStar.Tactics.Embedding.fs'.
     No implicit rule found for `tactics/FStar.Tactics.Embedding.fs'.
     Finished prerequisites of target file `tactics/FStar.Tactics.Embedding.fs'.
    No need to remake target `tactics/FStar.Tactics.Embedding.fs'.
    Considering target file `tactics/FStar.Tactics.Native.fs'.
     Looking for an implicit rule for `tactics/FStar.Tactics.Native.fs'.
     No implicit rule found for `tactics/FStar.Tactics.Native.fs'.
     Finished prerequisites of target file `tactics/FStar.Tactics.Native.fs'.
    No need to remake target `tactics/FStar.Tactics.Native.fs'.
    Pruning file `boot/FStar.Tactics.Interpreter.fst'.
   Finished prerequisites of target file `extract_tactics'.
  Must remake target `extract_tactics'.
../bin/fstar-any.sh --hint_info --eager_inference --lax --MLish --no_location_info --odir ocaml-output --codegen OCaml --include ../ulib --include boot --include basic --include extraction --include format --include fsdoc --include fstar --include parser --include prettyprint --include reflection --include smtencoding --include syntax --include tactics --include tosyntax --include typechecker ../ulib/FStar.Tactics.Types.fsti tactics/FStar.Tactics.Types.fs tactics/FStar.Tactics.Basic.fs tactics/FStar.Tactics.Embedding.fs tactics/FStar.Tactics.Native.fs boot/FStar.Tactics.Interpreter.fst --extract_namespace FStar.Tactics --no_extract FStar.Tactics.Native
Putting child 0x7fa5bb6056b0 (extract_tactics) PID 8548 on the chain.
Live child 0x7fa5bb6056b0 (extract_tactics) PID 8548 
/Users/vincentcheval/Documents/Recherche/Outils/FStar/src/boot/FStar.Util.fsti(32,11-32,19): (Error) Identifier not found: [System.DateTime]
Module System does not belong to the list of modules in scope, namely FStar.BaseTypes, FStar.Char, FStar.Float, FStar.UInt8, FStar.Int8, FStar.Int16, FStar.UInt16, FStar.Int32, FStar.Int64, FStar.Int, FStar.UInt64, FStar.UInt32, FStar.UInt, FStar.BitVector, FStar.Math.Lemmas, FStar.Math.Lib, FStar.Seq, FStar.Seq.Properties, FStar.Seq.Base, FStar.List.Tot, FStar.List.Tot.Properties, FStar.List.Tot.Base, FStar.Mul, FStar.All, FStar.ST, FStar.Heap, FStar.Monotonic.Heap, FStar.TSet, FStar.PredicateExtensionality, FStar.PropositionalExtensionality, FStar.StrongExcludedMiddle, FStar.Preorder, FStar.Set, FStar.FunctionalExtensionality, FStar.Classical, FStar.Squash, FStar.Exn, FStar.Pervasives, FStar.Pervasives.Native, Prims
1 error was reported (see above)
Reaping losing child 0x7fa5bb6056b0 PID 8548 
make[1]: *** [extract_tactics] Error 1
Removing child 0x7fa5bb6056b0 PID 8548 from chain.
Reaping losing child 0x7fbae47007a0 PID 8538 
make: *** [ocaml] Error 2
Removing child 0x7fbae47007a0 PID 8538 from chain.
catalin-hritcu commented 6 years ago

@cpitclaudel Is this issue still relevant or can it be closed?