Merge branch 'master' into santiago_examples

.docker/build/config-binaries.json

@@ -18,6 +18,7 @@
     "CIBuildTarget" : "fstar-binary-build",
     "NightlyBuildTarget" : "fstar-binary-build",
     "HasLogsToExtract" : true,
+    "HasQueryStats" : false,
 
     "NotificationEnabled" : true,
     "NotificationChannel" : "#fstar-build",

.docker/build/config-docs.json

@@ -18,6 +18,7 @@
     "CIBuildTarget" : "fstar-docs",
     "NightlyBuildTarget" : "fstar-docs",
     "HasLogsToExtract" : true,
+    "HasQueryStats" : false,
 
     "NotificationEnabled" : true,
     "NotificationChannel" : "#fstar-build",

INSTALL.md

@@ -49,6 +49,24 @@ Building F\* from sources section below) or at least in the latest
 [F\* binaries on GitHub]: https://github.com/FStarLang/FStar/releases
 [automatic weekly builds]: https://github.com/FStarLang/binaries/tree/master/weekly
 
+### Extracting F* programs to OCaml using binary releases
+
+Binary builds come with binary builds of F* standard library. 
+These can only be linked against code compiled in **exactly the same OCaml environment**.
+A common symptom of a mismatch is a message of the form 
+
+       Error: Files bin/fstarlib/fstarlib.cmxa
+              and ...
+              make inconsistent assumptions over interface ...
+
+Rather, if you intend to extract and compile OCaml code against the F* library, please 
+rebuild it with:
+
+        $ make -C ulib/ml
+
+See [here](https://github.com/FStarLang/FStar/wiki/Executing-F*-code) for further 
+documentation on extracting and executing F* code.
+
 ### Testing a binary package ###
 
 Test that the binary is good by expanding the archive and running the

doc/tutorial/code/exercises/Ex01a.fst.hints

@@ -18,7 +18,7 @@
         "projection_inverse_FStar.Pervasives.V_v"
       ],
       0,
-      "6b11d730c8ed4f30624f77e21a6b4737"
+      "c3681979915fd4d6c4afb9ab675f43f9"
     ],
     [
       "Ex01a.checkedRead",
@@ -27,7 +27,7 @@
       1,
       [ "@query", "projection_inverse_BoxBool_proj_0" ],
       0,
-      "968e22e40200dd508b2e075c9f658d60"
+      "f38ce00949685548a0ca376e1c50eb8d"
     ]
   ]
 ]

doc/tutorial/code/exercises/Ex10a.fst.hints

@@ -94,7 +94,7 @@
         "typing_Tm_abs_34ef4ead09ec7d33c614d4dffaa96c6e", "unit_typing"
       ],
       0,
-      "5ee03e8889ac1f9ea24bc4935d5213a1"
+      "26e4c1483d5b717691f849d19b1bf412"
     ],
     [
       "Ex10a.__proj__Readable__item___0",
@@ -107,7 +107,7 @@
         "refinement_interpretation_Tm_refine_43c663371132c0c847de0562111b3034"
       ],
       0,
-      "bf5580a465fd246986d4e696fbde7308"
+      "dc4e56f25c247234dbfcdf4f436b0ae6"
     ],
     [
       "Ex10a.__proj__Writable__item___0",
@@ -120,7 +120,7 @@
         "refinement_interpretation_Tm_refine_b7c189cb365c663bbaaab1bb8e2e94da"
       ],
       0,
-      "4611c0316af9a54de07f1e5c8ce0b412"
+      "7fa1d7991fb61b331e612c36f9c26bc2"
     ],
     [
       "Ex10a.canRead",
@@ -133,7 +133,7 @@
         "fuel_guarded_inversion_Ex10a.entry"
       ],
       0,
-      "8d5f6d26403af903bfa4259066239816"
+      "d2cbec38a02f651ce889f27d66d33036"
     ],
     [
       "Ex10a.revoke",
@@ -146,7 +146,7 @@
         "refinement_interpretation_Ex10a_Tm_refine_f978ff754af8f266cb4edc62e2a055cb"
       ],
       0,
-      "0fb59d90ef4abe799611f0b3d098ee62"
+      "d6b66ef73acb9058ef5757281843cd94"
     ]
   ]
 ]

doc/tutorial/code/exercises/Ex12a1.Cap.fst.hints

@@ -8,7 +8,7 @@
       1,
       [ "@query", "assumption_Platform.Bytes.HasEq_bytes" ],
       0,
-      "49d4f6941c285ef6c4f235d50f8d9b08"
+      "9e0ac175f69fbb77d1e22fa14b836279"
     ],
     [
       "Ex12a1.Cap.capRead",
@@ -17,7 +17,7 @@
       1,
       [ "@query", "assumption_Platform.Bytes.HasEq_bytes" ],
       0,
-      "5614c8c65aa6beb3be2807762f501898"
+      "6eac32bada1e282cfeecb03027a2116b"
     ]
   ]
 ]

doc/tutorial/code/exercises/Ex12b1.Format.fst.hints

@@ -8,7 +8,7 @@
       1,
       [ "@query", "assumption_FStar.UInt8.t__uu___haseq" ],
       0,
-      "6461faf1e918277a91904f586c95255c"
+      "5a4062cee7166c50e29e32cf47b49dac"
     ],
     [
       "Ex12b1.Format.append_inj_lemma",
@@ -29,7 +29,7 @@
         "typing_FStar.Seq.Base.eq", "typing_FStar.Seq.Base.op_At_Bar"
       ],
       0,
-      "4dedd9334a5dd050876706210cce31f0"
+      "a31df6bccc2b08447c9ea7f6c377f95c"
     ],
     [
       "Ex12b1.Format.lemma_eq_intro",
@@ -46,7 +46,7 @@
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
       ],
       0,
-      "702b024e31d39d602bad4600bceff490"
+      "2163ea6d28c5042ffa39f2937ae614c6"
     ],
     [
       "Ex12b1.Format.lemma_eq_intro",
@@ -55,7 +55,7 @@
       1,
       [ "@query", "lemma_FStar.Seq.Base.lemma_eq_intro" ],
       0,
-      "89bf9cbf44347ef113064e8a4b01f845"
+      "ed99b5dd2bdd3c4d755414fc6bdac725"
     ],
     [
       "Ex12b1.Format.UTF8_inj",
@@ -64,7 +64,7 @@
       1,
       [ "@query", "assumption_FStar.UInt8.t__uu___haseq" ],
       0,
-      "eade737dfc72bd2fcc8aa8a558f0e794"
+      "cc88bf82c583f3682114d566a9c60a7c"
     ],
     [
       "Ex12b1.Format.uint16_to_bytes",
@@ -73,7 +73,7 @@
       1,
       [ "@query", "equation_Ex12b1.Format.uInt16" ],
       0,
-      "96a8923143be1d96b1631426861126f0"
+      "b263f9ef5eea0abaeb8fe08494d6ff37"
     ],
     [
       "Ex12b1.Format.uint16_to_bytes",
@@ -82,7 +82,7 @@
       1,
       [ "@query", "equation_Ex12b1.Format.uInt16" ],
       0,
-      "969b88b87c1dcfff28e763bd55ada6b8"
+      "202e5daed47c91b08fec51ab4d6d4efd"
     ],
     [
       "Ex12b1.Format.uint16_to_bytes",
@@ -98,7 +98,7 @@
         "refinement_interpretation_Ex12b1.Format_Tm_refine_9adbdccb31bd5d6d35b7a0e150a5d273"
       ],
       0,
-      "f834fa9a57b68ab583c729467caacb89"
+      "ce175fb3568fcc127e2a1283bba84063"
     ],
     [
       "Ex12b1.Format.UINT16_inj",
@@ -114,7 +114,7 @@
         "refinement_interpretation_Ex12b1.Format_Tm_refine_840eba52f90cf7bf85387b7d8eff7d06"
       ],
       0,
-      "843b8b7a5306b1b64de87a2b61563626"
+      "9506c817770b277834154e000c21b496"
     ],
     [
       "Ex12b1.Format.response",
@@ -127,7 +127,7 @@
         "refinement_interpretation_Tm_refine_0b0c7870479b009ecde2e1ac3a590e38"
       ],
       0,
-      "7deb998d1c48b5178b2d2633ad7fb3a8"
+      "2f7026e8baaf47326e4b5aa8d53cc49b"
     ],
     [
       "Ex12b1.Format.append_inj_lemma",
@@ -136,7 +136,7 @@
       1,
       [ "@query", "assumption_FStar.UInt8.t__uu___haseq" ],
       0,
-      "734c38c9dbe8ff3b7b1677a8b127d13b"
+      "31d3562e4bf45006c03bbd3e83dddf3f"
     ],
     [
       "Ex12b1.Format.lemma_eq_intro",
@@ -153,7 +153,7 @@
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
       ],
       0,
-      "bcaf5e2c1aed17bb899b4b55d02b569b"
+      "4ccb5e1a8aefe3150342309f290c0056"
     ],
     [
       "Ex12b1.Format.UTF8_inj",
@@ -162,7 +162,7 @@
       1,
       [ "@query", "assumption_FStar.UInt8.t__uu___haseq" ],
       0,
-      "1710743a02da700edcad58bbd949d9ef"
+      "07a711e2ac6a45cb7d3a9a476e289b77"
     ],
     [
       "Ex12b1.Format.uint16_to_bytes",
@@ -171,7 +171,7 @@
       1,
       [ "@query", "equation_Ex12b1.Format.uInt16" ],
       0,
-      "92b8da4cfc3bad0bf105b4ef49956751"
+      "4bfff80959e4b5f089befecb54aab83f"
     ],
     [
       "Ex12b1.Format.uint16_to_bytes",
@@ -180,7 +180,7 @@
       1,
       [ "@query", "equation_Ex12b1.Format.uInt16" ],
       0,
-      "caaae82fd18c9e66a2c784a98c31ffd7"
+      "76e34aa1f6fba783f76f779d29d084b9"
     ],
     [
       "Ex12b1.Format.uint16_to_bytes",
@@ -189,7 +189,7 @@
       1,
       [ "@query", "equation_Ex12b1.Format.uInt16" ],
       0,
-      "a985a1e884b2298c7b5ed423fd45b0cf"
+      "668035690c1c804e33d03d2dde71cf4f"
     ],
     [
       "Ex12b1.Format.UINT16_inj",
@@ -205,7 +205,7 @@
         "refinement_interpretation_Ex12b1.Format_Tm_refine_840eba52f90cf7bf85387b7d8eff7d06"
       ],
       0,
-      "c7f5075760805671efd7118db1fcde7e"
+      "1a25d11fe494443b54f9b6266888cdcd"
     ],
     [
       "Ex12b1.Format.response",
@@ -218,7 +218,7 @@
         "refinement_interpretation_Tm_refine_0b0c7870479b009ecde2e1ac3a590e38"
       ],
       0,
-      "0649b0b5c834c440d0d0cd692a6cb34d"
+      "db8c9e97f39481c8d9be345288a46f94"
     ]
   ]
 ]