Merge pull request #52 from arnoudvanderleer/CI

Make CI work for the coq files

.github/workflows/build-schools.yml

@@ -2,36 +2,67 @@
 
 name: CI
 
-# Controls when the action will run. 
+# Controls when the action will run.
 on:
   # Triggers the workflow on push or pull request events but only for the master branch
   push:
     branches: [ master ]
   pull_request:
     branches: [ master ]
 
+  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
+
   # Allows you to run this workflow 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
 
     # Steps represent a sequence of tasks that will be executed as part of the job
     steps:
-      # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
-      - uses: actions/checkout@v2
-
-
-      # Install everything needed for building UniMath (and more)
-      - name: Install build dependencies
-        run: sudo apt-get install build-essential git ocaml ocaml-nox ocaml-native-compilers camlp5 libgtk2.0 libgtksourceview2.0 liblablgtk-extras-ocaml-dev ocaml-findlib libnum-ocaml-dev emacs
-
-      # Change into UniMath directory and build UniMath
-      - name: Build UniMath and Schools files
-        run: |
-          cd $GITHUB_WORKSPACE
-          time make 
+      # Checkout UniMath into the working directory
+      - name: Checkout UniMath.
+        uses: actions/checkout@v3
+        with:
+          repository: UniMath/UniMath
+          clean: false
+          path: .
+
+      # Checkout the current branch into Schools/
+      - name: Checkout Schools.
+        uses: actions/checkout@v3
+        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
+        with:
+          ocaml-compiler: ocaml-variants.4.14.0+options,ocaml-option-flambda
+          dune-cache: true
+          opam-disable-sandboxing: true
+
+      - name: Install Dune
+        run: opam pin add dune ${{ env.dune-version }}
+      - name: Install Coq
+        run: opam pin add coq ${{ env.coq-version }}
+
+      # Schools is built using the flags specified in code/dune.
+      - name: Compile Schools.
+        run: opam exec -- dune build Schools --display=short --error-reporting=twice

2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v

@@ -47,10 +47,10 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you think there are too many hits and 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
@@ -62,14 +62,14 @@ 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.
 
 (** *** 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 *)
@@ -101,7 +101,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 *)
@@ -404,7 +404,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]? *)
-    Search (_ × _).
+    (* Search (_ × _). *)
     (** No hope at all for our equation - we can only hope
         for weak equivalence. *)
 Abort.

2017-12-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v

@@ -47,10 +47,10 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything that *involves* booleans, then do *)
-  Search bool.
+  (* Search bool. *)
   (** If you think there are too many hits and 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
@@ -62,14 +62,14 @@ 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.
 
 (** *** 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 *)
@@ -101,7 +101,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 *)
@@ -369,9 +369,9 @@ 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 [pathsinv0l] that has [idpath] in its conclusion. *)
-SearchRewrite idpath.
+(* SearchRewrite idpath. *)
 (** No result! *)
 
 (** *** How to decompose formulas *)
@@ -504,11 +504,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(_ × _). *)
     (** No hope at all - we can only hope for weak equivalence. *)
 Abort.
 
-SearchPattern(_ ≃ _).
+(* SearchPattern(_ ≃ _). *)
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.

2017-12-Birmingham/Part6_Category_Theory/category_theory_exercises.v

@@ -6,15 +6,18 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
+Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
+Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 

2017-12-Birmingham/Part6_Category_Theory/category_theory_solutions.v

@@ -7,15 +7,18 @@
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.Core.Setcategories.
-Require Import UniMath.CategoryTheory.categories.HSET.Core.
+Require Import UniMath.CategoryTheory.Categories.HSET.Core.
+Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
+Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
+Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.FinOrdProducts.
-Require Import UniMath.CategoryTheory.limits.equalizers.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.FinOrdProducts.
+Require Import UniMath.CategoryTheory.Limits.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 

2017-12-Birmingham/dune

@@ -0,0 +1,11 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Birmingham2017)
+ (flags :standard
+        -noinit
+        -indices-matter
+        -type-in-type
+        -w -notation-overridden)
+ (theories UniMath))
+

2019-04-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.v

@@ -470,7 +470,7 @@ 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 _ (_ -> _ -> _). *)

2019-04-Birmingham/Part3_Univalent_Foundations/truncation_exercices.v

@@ -69,8 +69,8 @@ Definition parity (n : nat) := nat_rect (fun _ => nat) 0 (fun _ b => flip b) n.
    notion of image in which we replace ∑ with ∃. *)
 Require Import UniMath.Foundations.Propositions.
 
-Definition image {A B : UU} (f : A → B) :
-  ∑ (y : B), ∃ (x : A), f x = y.
+Definition image {A B : UU} (f : A → B) : UU
+  := ∑ (y : B), ∃ (x : A), f x = y.
 
 (* Prove that the (univalent) image of partiy is equivalent to Bool. *)
 Theorem image_parity_equiv_bool :

2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics.v

@@ -48,9 +48,9 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything 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
@@ -62,14 +62,14 @@ 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.
 
 (** *** 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 *)
@@ -102,7 +102,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. *)
@@ -395,7 +395,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]? *)
-    Search (_ × _).
+    (* Search (_ × _). *)
     (** No hope at all for our equation - we can only hope
         for weak equivalence. *)
 Abort.

2019-04-Birmingham/Part4_Tactics_UniMath/lecture_tactics_long_version.v

@@ -49,9 +49,9 @@ Definition myfirsttruthvalue: bool.
 Proof.
   (** Now we still have to give the term, but we are in interactive mode. *)
   (** If you want to see everything 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.
 (** [myfirsttruthvalue relies on an unsafe universe hierarchy] is output to indicate
@@ -74,7 +74,7 @@ Print myfirsttruthvalue.
 (** *** 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 *)
@@ -107,7 +107,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. *)
@@ -360,9 +360,9 @@ 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 [maponpathsinv0] that has [idpath] in its conclusion. *)
-SearchRewrite idpath.
+(* SearchRewrite idpath. *)
 (** No result! *)
 
 (** *** How to decompose formulas *)
@@ -500,11 +500,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(_ × _). *)
     (** No hope at all - we can only hope for weak equivalence. *)
 Abort.
 
-SearchPattern(_ ≃ _).
+(* SearchPattern(_ ≃ _). *)
 Print weqcomp.
 Print weqdirprodasstor.
 Print weqdirprodasstol.