feat(ci): script and ci check F* versions

cryspen · Jan 18, 2024 · a65106d · a65106d
1 parent c8198a0
commit a65106d
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 7 deletions.
diff --git a/.github/workflows/install_and_test.yml b/.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

diff --git a/examples/README.md b/examples/README.md
@@ -16,7 +16,7 @@
   * 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* `v2023.09.03`<!---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;

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -9,7 +9,7 @@
       };
     };
     rust-overlay.follows = "crane/rust-overlay";
-    fstar-flake = {
+    fstar = {
       url = "github:FStarLang/FStar/v2024.01.13";
       inputs = {
         nixpkgs.follows = "nixpkgs";
@@ -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" ''