Improve the build script, re-enable Search commands

.github/workflows/build-schools.yml

@@ -1,68 +1,84 @@
-# This is a basic workflow to help you get started with Actions
-
 name: CI
 
 # Controls when the action will run.
 on:
-  # Triggers the workflow on push or pull request events but only for the master branch
+  # Run the workflow on push or pull request events but only for the master branch
   push:
     branches: [ master ]
   pull_request:
     branches: [ master ]
 
+  # Run at 05:37 UTC every Thursday to keep the cache from being evicted.
   schedule:
-    # Run this workflow at 02:15 UTC every Tuesday to keep the cache from being
-    # evicted. A typical run with everything cached should take less than 10
-    # minutes.
-    - cron: 15 2 * * TUE
+    - cron: 37 5 * * THU
 
-  # Allows you to run this workflow manually from the Actions tab
+  # Run when activated manually from the Actions tab
   workflow_dispatch:
 
-env:
-  # Set this to the version of Coq that should be used.
-  coq-version: 8.19.0
-  dune-version: 3.8.0
-  DUNE_CACHE_STORAGE_MODE: copy
-
-# A workflow run is made up of one or more jobs that can run sequentially or in parallel
 jobs:
-  # This workflow contains a single job called "build"
   build:
-    name: Build Schools
-    # The type of runner that the job will run on
-    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ ubuntu-latest ]
+        coq-version: [ latest ]
+        ocaml-version: [ default ]
 
-    # Steps represent a sequence of tasks that will be executed as part of the job
+    name: Build Schools on Linux (Coq ${{ matrix.coq-version }})
+    runs-on: ${{ matrix.os }}
     steps:
-      # Checkout UniMath into the working directory
       - name: Checkout UniMath.
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: UniMath/UniMath
           clean: false
           path: .
 
-      # Checkout the current branch into Schools/
       - name: Checkout Schools.
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: Schools
 
-      # Ideally we would use docker-coq. A setup currently takes about 7min
-      # before it starts compiling, with OCaml cached.
-      - name: Install OCaml.
-        uses: ocaml/setup-ocaml@v2
+      # The path variable here matches the DUNE_CACHE_ROOT variable in the "Build Schools" step
+      - name: Load cache
+        uses: actions/cache/restore@v4
+        id: cache
+        with:
+          path: dune-cache
+          key: UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}
+          restore-keys: |
+            UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}
+            UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-
+
+      - name: Build Schools
+        uses: coq-community/docker-coq-action@v1
         with:
-          ocaml-compiler: ocaml-variants.4.14.0+options,ocaml-option-flambda
-          dune-cache: true
-          opam-disable-sandboxing: true
+          coq_version: ${{ matrix.coq-version }}
+          ocaml_version: ${{ matrix.ocaml-version }}
+          custom_script: |
+            startGroup "Workaround permission issue"
+              sudo chown -R coq:coq .
+            endGroup
 
-      - name: Install Dune
-        run: opam pin add dune ${{ env.dune-version }}
-      - name: Install Coq
-        run: opam pin add coq ${{ env.coq-version }}
+            startGroup "Print versions"
+              opam --version
+              opam exec -- dune --version
+              opam exec -- coqc --version
+            endGroup
 
-      # Schools is built using the flags specified in code/dune.
-      - name: Compile Schools.
-        run: opam exec -- dune build Schools --display=short --error-reporting=twice
+            startGroup "Build UniMath"
+              export DUNE_CACHE_ROOT=$(pwd)/dune-cache/
+              opam exec -- dune build Schools -j 2 --display=short --cache=enabled --error-reporting=twice
+            endGroup
+
+      # In a separate step, to make sure it runs, even if the previous step fails
+      - name: Revert permissions
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+
+      - name: Save cache
+        uses: actions/cache/save@v4
+        if: ${{ always() }}
+        with:
+          path: dune-cache
+          key: UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}

2024-07-Minneapolis/2_Coq/fundamentals_lecture.v

@@ -572,10 +572,10 @@ in UniMath it is very important to be able to search the library so
 that you don't do something someone else has already done. *)
 
 (** To find everything about nat type: *)
-(* Search nat. *)
+Search nat.
 
 (** To search for all lemmas involving the pattern *)
-(* Search _ (_ -> _ -> _). *)
+Search _ (_ -> _ -> _).
 
 (** To find information about a notation *)
 Locate "+".

2024-07-Minneapolis/4_Tactics/tactics_lecture.v

@@ -42,9 +42,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  (* Search bool. *)
+  Search bool.
   (** If you only want to find library elements that *yield* booleans, then try *)
-  (* SearchPattern bool. *)
+  SearchPattern bool.
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -56,15 +56,15 @@ Defined.
 
 (** [Defined.] instructs Coq to complete the whole interactive construction of a term,
     verify it and to associate it with the given identifer, here [myfirsttruthvalue]. *)
-(* Search bool. *)
+Search bool.
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
 
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -97,7 +97,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -384,7 +384,7 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    (* SearchPattern (_ × _ =  _ × _). *)
+    SearchPattern (_ × _ =  _ × _).
     (** Nothing for our equation - we can only hope for weak equivalence ≃,
         see the exercises. *)
 Abort.

2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v

@@ -49,9 +49,9 @@ Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything in the currently loaded part of the UniMath library
       that *involves* booleans, then do *)
-  (* Search bool. *)
+  Search bool.
   (** If you only want to find library elements that *yield* booleans, then try *)
-  (* SearchPattern bool. *)
+  SearchPattern bool.
   (** [true] does not take an argument, and it is already a term we can take as definiens. *)
   exact true.
   (** [exact] is a tactic which takes the term as argument and informs Coq in the proof mode to
@@ -65,7 +65,7 @@ Defined.
     verify it and to associate it with the given identifer, here [myfirsttruthvalue].
     This may go wrong for different reasons, including implementation errors of the Coq
     system - that will not affect trustworthiness of the library. *)
-(* Search bool. *)
+Search bool.
 (** The new definition appears at the beginning of the list. *)
 Print myfirsttruthvalue.  (** or just point to the identifier and hit the
                               key combination mentioned in Part 2 *)
@@ -76,7 +76,7 @@ Print myfirsttruthvalue.  (** or just point to the identifier and hit the
 (** *** a more compelling example *)
 Definition mysecondtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply negb.
   (** applies the function [negb] to obtain the required boolean,
       thus the system has to ask for its argument *)
@@ -109,7 +109,7 @@ Definition andb (b1 b2: bool) : bool := if b1 then b2 else false.
 
 Definition mythirdtruthvalue: bool.
 Proof.
-  (* Search bool. *)
+  Search bool.
   apply andb.
   (** [apply andb.] applies the function [andb] to obtain the required boolean,
       thus the system has to ask for its TWO arguments, one by one. *)
@@ -359,7 +359,7 @@ Print paths.
 (** A word of warning for those who read "Coq in a Hurry": [SearchRewrite]
     does not find equations w.r.t. this notion, only w.r.t. Coq's built-in
     propositional equality. *)
-(* SearchPattern (paths _ _). *)
+SearchPattern (paths _ _).
 (** Among the search results is [pathsinv0r] that has [idpath] in its conclusion. *)
 (* SearchRewrite idpath. *)
 (** No result! *)
@@ -496,11 +496,11 @@ We need to help Coq with the argument [b] to [pathscomp0].
 *)
   apply (pathscomp0 (b := A × (B × (C × D)))).
   - (** is this not just associativity with third argument [C × D]? *)
-    (* SearchPattern (_ × _ =  _ × _). *)
+    SearchPattern (_ × _ =  _ × _).
     (** Nothing for our equation - we can only hope for weak equivalence ≃. *)
 Abort.
 
-(* SearchPattern(_ ≃ _). *)
+SearchPattern(_ ≃ _).
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.

2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v

@@ -194,7 +194,7 @@ Admitted.
 Definition ptdset_iso_weq (X Y : ptdset) : (X ╝ Y) ≃ (ptdset_iso X Y).
 Proof.
   use weqtotal2.
-  + (* Search ( (_ = _) ≃ ( _ ≃ _)). *)
+  + Search ( (_ = _) ≃ ( _ ≃ _)).
     (* Solve this goal. *)
     admit.
   + (* Solve this goal. *)
@@ -277,7 +277,7 @@ Proof.
   unfold monoidiso'.
   unfold monoidiso.
   (* Observe that this is just an reassociation of Sigma-types. *)
-  (* Search ( (∑ _ , _ ) ≃ _ ). *)
+  Search ( (∑ _ , _ ) ≃ _ ).
   admit.
 Admitted.
 

2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v

@@ -217,7 +217,7 @@ Defined.
 Definition ptdset_iso_weq (X Y : ptdset) : (X ╝ Y) ≃ (ptdset_iso X Y).
 Proof.
   use weqtotal2.
-  + (* Search ( (_ = _) ≃ ( _ ≃ _)). *)
+  + Search ( (_ = _) ≃ ( _ ≃ _)).
     use hSet_univalence.
   + intro p.
     induction X as [X x].
@@ -257,7 +257,7 @@ Local Open Scope multmonoid.
 Notation "x * y" := (op x y) : multmonoid.
 Notation "1" := (unel _) : multmonoid.
 
-(* Search monoid. *)
+Search monoid.
 
 (*
   Construct the following chain of equivalences

2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v

@@ -311,7 +311,7 @@ Section Exercise_2.
     : is_univalent pointed_operation_set.
   Proof.
     apply is_univalent_total_category.
-    - (* Search HSET. *)
+    - Search HSET.
       exact is_univalent_HSET.
     - exact pointed_operation_is_univalent_disp.
   Defined.