Merge pull request #441 from hacspec/update-fstar-version

Update F* version to latest release

.github/workflows/install_and_test.yml

@@ -24,6 +24,10 @@ jobs:
         nix profile install .#rustc
         nix profile install .
         
+    - name: Ensure readme coherency
+      run: |
+        nix build .#check-readme-coherency -L
+
     - name: Test the toolchain
       run: |
         nix build .#check-toolchain -L

.gitignore

@@ -3,7 +3,6 @@ target/
 **/*.rs.bk
 node_modules
 TODO.org
-.envrc
 .direnv
 _build
 result

examples/.envrc

@@ -0,0 +1 @@
+use flake .#fstar

examples/README.md

@@ -13,10 +13,10 @@
 
   First, make sure to have hax installed in PATH. Then:
 
-  * With Nix, `nix develop .#fstar-examples` setups a shell automatically for you.
+  * With Nix, `nix develop .#fstar` setups a shell automatically for you.
 
   * Without Nix:
-    1. install F* `v2023.09.03` manually (see https://github.com/FStarLang/FStar/blob/master/INSTALL.md);
+    1. install F* `v2024.01.13`<!---FSTAR_VERSION--> manually (see https://github.com/FStarLang/FStar/blob/master/INSTALL.md);
        1. make sure to have `fstar.exe` in PATH;
        2. or set the `FSTAR_HOME` environment variable.
     2. clone [Hacl*](https://github.com/hacl-star/hacl-star) somewhere;

flake.nix

@@ -9,8 +9,8 @@
       };
     };
     rust-overlay.follows = "crane/rust-overlay";
-    fstar-flake = {
-      url = "github:FStarLang/FStar/v2023.09.03";
+    fstar = {
+      url = "github:FStarLang/FStar/v2024.01.13";
       inputs = {
         nixpkgs.follows = "nixpkgs";
         flake-utils.follows = "flake-utils";
@@ -27,10 +27,9 @@
     nixpkgs,
     rust-overlay,
     crane,
-    fstar-flake,
     hacl-star,
     ...
-  }:
+  } @ inputs:
     flake-utils.lib.eachDefaultSystem (
       system: let
         pkgs = import nixpkgs {
@@ -41,7 +40,7 @@
         craneLib = (crane.mkLib pkgs).overrideToolchain rustc;
         ocamlformat = pkgs.ocamlformat_0_24_1;
         rustfmt = pkgs.rustfmt;
-        fstar = fstar-flake.packages.${system}.default;
+        fstar = inputs.fstar.packages.${system}.default;
       in rec {
         packages = {
           inherit rustc ocamlformat rustfmt fstar;
@@ -59,15 +58,37 @@
 
           check-toolchain = checks.toolchain;
           check-examples = checks.examples;
+          check-readme-coherency = checks.readme-coherency;
         };
         checks = {
           toolchain = packages.hax.tests;
           examples = pkgs.callPackage ./examples {
             inherit (packages) hax;
             inherit craneLib fstar hacl-star;
           };
+          readme-coherency = let
+            src = pkgs.lib.sourceFilesBySuffices ./. [".md"];
+          in
+            pkgs.stdenv.mkDerivation {
+              name = "readme-coherency";
+              inherit src;
+              buildPhase = ''
+                ${apps.replace-fstar-versions-md.program}
+                diff -r . ${src}
+              '';
+              installPhase = "touch $out";
+            };
         };
         apps = {
+          replace-fstar-versions-md = {
+            type = "app";
+            program = "${pkgs.writeScript "replace-fstar-versions-md" ''
+              FSTAR_VERSION=$(cat ${./flake.lock} | ${pkgs.jq}/bin/jq '.nodes.fstar.original.ref' -r)
+              ${pkgs.fd}/bin/fd \
+                 -X ${pkgs.sd}/bin/sd '`.*?`(<!---FSTAR_VERSION-->)' '`'"$FSTAR_VERSION"'`$1' **/*.md \
+                 ";" --glob '*.md'
+            ''}";
+          };
           serve-rustc-docs = {
             type = "app";
             program = "${pkgs.writeScript "serve-rustc-docs" ''
@@ -116,7 +137,7 @@
           ];
           LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib";
         in {
-          fstar-examples = pkgs.mkShell {
+          fstar = pkgs.mkShell {
             inherit inputsFrom LIBCLANG_PATH;
             HACL_HOME = "${hacl-star}";
             packages = packages ++ [fstar];

proof-libs/fstar/.envrc

@@ -0,0 +1 @@
+use flake .#fstar