From 322986e82d2c860abd00bc1fa2793eeb4a01064d Mon Sep 17 00:00:00 2001 From: Tempestas Ludi Date: Wed, 28 Aug 2024 21:07:45 +0200 Subject: [PATCH 1/3] Create a new build script, based on the UniMath one --- .github/workflows/build-schools.yml | 92 +++++++++++++++++------------ 1 file changed, 54 insertions(+), 38 deletions(-) diff --git a/.github/workflows/build-schools.yml b/.github/workflows/build-schools.yml index 79c0c34..f04b24d 100644 --- a/.github/workflows/build-schools.yml +++ b/.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 }} From 2d4c5dec6bdc4c84a395456ff05dfb41a8e9fcdf Mon Sep 17 00:00:00 2001 From: Tempestas Ludi Date: Wed, 28 Aug 2024 21:15:12 +0200 Subject: [PATCH 2/3] Re-enable instances of Search in the 2024 directory --- 2024-07-Minneapolis/4_Tactics/tactics_lecture.v | 12 ++++++------ .../4_Tactics/tactics_lecture_extended.v | 16 ++++++++-------- .../set_level_mathematics_exercises.v | 4 ++-- .../set_level_mathematics_solutions.v | 4 ++-- .../category_theory_solutions.v | 2 +- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/2024-07-Minneapolis/4_Tactics/tactics_lecture.v b/2024-07-Minneapolis/4_Tactics/tactics_lecture.v index cce9bc6..3e6661c 100644 --- a/2024-07-Minneapolis/4_Tactics/tactics_lecture.v +++ b/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,7 +56,7 @@ 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 *) @@ -64,7 +64,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 *) @@ -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. diff --git a/2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v b/2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v index 2d4e8e8..d095e94 100644 --- a/2024-07-Minneapolis/4_Tactics/tactics_lecture_extended.v +++ b/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. diff --git a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v index e159212..6bb77e5 100644 --- a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_exercises.v +++ b/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. diff --git a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v b/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v index e8a2786..7b76166 100644 --- a/2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v +++ b/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 diff --git a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v b/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v index da5ee3f..739f587 100644 --- a/2024-07-Minneapolis/6_Category-theory-in-UF/category_theory_solutions.v +++ b/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. From f93eaf36f6aac2c6767d1cb5afba797949252de8 Mon Sep 17 00:00:00 2001 From: Tempestas Ludi Date: Wed, 28 Aug 2024 21:20:24 +0200 Subject: [PATCH 3/3] Re-enable Search in the 2024 file fundamentals_lecture --- 2024-07-Minneapolis/2_Coq/fundamentals_lecture.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v b/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v index f5cb2a8..100a612 100644 --- a/2024-07-Minneapolis/2_Coq/fundamentals_lecture.v +++ b/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 "+".