Use opam package coq-library-undecidability.1.0.1+8.16

Author: yforster

.github/workflows/build.yml

@@ -33,5 +33,5 @@ jobs:
 
       - run: opam repo add coq-released https://coq.inria.fr/opam/released
       - run: opam update
-      - run: opam pin add coq-library-undecidability.dev+8.16 "https://github.com/uds-psl/coq-library-undecidability.git#coq-8.16"
+      - run: opam install coq-library-undecidability.1.0.1+8.16
       - run: opam exec -- make all -j2 TIMED=1

README.md

@@ -17,36 +17,27 @@ This library contains complexity theory. It is built upon the [Coq Library of Un
 - `Libs`: internal library files used in multiple other directories
 
 ## Installation
-<!---### Install from opam
 
-Install the [A Coq Library of Undecidability Proofs](https://github.com/uds-psl/coq-library-undecidability), then install this.
---->
 ### Building from source
 
-There are two documented ways to install the dependencies of this library. This library depends on the [Coq Library of Undecidability Proofs](https://github.com/uds-psl/coq-library-undecidability), which is either provided as a git submodule or as opam package.
-
-The recommended way to install dependencies is to checkout the submodules of this git repository with `git submodule update --init --recursive` and install all dependencies of the complexity library using `make depssubmodule`. This has the benefit of only compiles the files of the undecidability library actually needed by the complexity library.
-
-Or use the `make depsopam` to install all dependencies using opam. The undecidability library is then automatically `opam pin`ned to a specific git hash. 
-
-
-<!---### Then, the [Coq Library of Undecidability Proofs](https://github.com/uds-psl/coq-library-undecidability)is included as a submodule in `./coq-library-undecidability`. -->
+This library depends on the [Coq Library of Undecidability Proofs](https://github.com/uds-psl/coq-library-undecidability) version 1.0.1. See the installation instructions of this library. It will suffice to install the `opam` package `coq-library-undecidability.1.0.1+8.16`, for instance by `opam install . --deps-only`.
 
 - `make all` builds the library and the dependencies
-- `make depssubmodule` builds the dependencies using the submodule for the undecidability library and opam for everything else
-- `make depsopam` builds the dependencies using opam for everything
 - `make html` generates clickable coqdoc `.html` in the `website` subdirectory
 - `make clean` removes all build files in `theories` and `.html` files in the `website` directory
-- `make realclean` removes the build files of the dependencies as well as everything `make clean` removes
 
 ### Troubleshooting
 
-#### Coq version
+#### Version of Coq and dependencies
 
-Be careful that this branch only compiles under Coq 8.15.
+Be careful that this branch only compiles under Coq 8.16
+and with the Coq Library of Undecidability Proofs, version 1.0.1.
+Newer versions of the library are not supported, in particular versions 1.1 and upwards are not supported.
 
 ## Published work and technical reports
 
+- Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. Lennard Gäher, Fabian Kunze. ITP 2021. Subdirectory `NP/SAT`. https://doi.org/10.4230/LIPIcs.ITP.2021.20
+- A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke. ITP 2021. Subdirectories `L/TM` and `TM`. https://doi.org/10.4230/LIPIcs.ITP.2021.19
 - Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. Fabian Kunze, Gert Smolka, and Yannick Forster. APLAS 2018. Subdirectory `L/AbstractMachines`. https://www.ps.uni-saarland.de/extras/cbvlcm2/
 - The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space.Yannick Forster, Fabian Kunze, Marc Roth. POPL 2020. Mechanised parts in `L/AbstractMachines` and `SpaceboundsTime.v` https://www.ps.uni-saarland.de/extras/wcbv-reasonable/
 
@@ -58,21 +49,12 @@ We use two frameworks which ease computability proofs with resource analysis for
 - A certifying extraction with time bounds from Coq to call-by-value lambda-calculus. ITP '19. https://github.com/uds-psl/certifying-extraction-with-time-bounds
 - Verified Programming of Turing Machines in Coq. Yannick Forster, Fabian Kunze, Maximilian Wuttke. Technical report. https://github.com/uds-psl/tm-verification-framework/
 
-<!---
-## How to contribute
-
-- Fork the project on GitHub.
-- Create a new subdirectory for your project and add your files.
-- Add a license for your project.
-- Edit the "Existing undecidable problems" and the "Contributors" section in this file
-- File a pull request.
---->
-
 ## Contributors
 
 - Fabian Kunze
 - Lennard Gäher
 - Maximilian Wuttke
 - Yannick Forster
+- Stefan Haan
 
 

opam

@@ -7,7 +7,8 @@ bug-reports: "https://github.com/uds-psl/coq-library-complexity/issues"
 authors: ["Fabian Kunze"
           "Lennard Gäher"
           "Maximilian Wuttke"
-          "Yannick Forster" ]
+          "Yannick Forster"
+          "Stefan Haan"]
 license: "CeCILL"
 build: [
   [make "-j%{jobs}%"]
@@ -19,8 +20,8 @@ remove: [
   ["rm" "-R" "%{lib}%/coq/user-contrib/Complexity"]
 ]
 depends: [
-  "coq" {= "8.16"}
-  "coq-library-undecidability" {>= "dev+8.16" }
+  "coq" {>= "8.16" & < "8.17"}
+  "coq-library-undecidability" {= "1.0.1+8.16" }
 ]
 
 synopsis: "A Coq Library of Complexity Theory"