Merge pull request #1 from coq-community/fix-8.12

Port to Coq 8.12, add boilerplate

.github/workflows/docker-ci.yml

@@ -0,0 +1,43 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.13'
+          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.11'
+          - 'coqorg/coq:8.10'
+          - 'coqorg/coq:8.9'
+          - 'coqorg/coq:8.8'
+          - 'coqorg/coq:8.7'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-goedel.opam'
+          custom_image: ${{ matrix.image }}
+          before_install: |
+            startGroup "Setup and print opam config"
+              opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+              opam config list; opam repo list; opam list
+            endGroup
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

.gitignore

@@ -0,0 +1,12 @@
+Makefile.coq
+Makefile.coq.conf
+_build
+*~
+*.d
+*.aux
+*.glob
+*.vo
+*.vio
+*.vok
+*.vos
+.lia.cache

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2007-present Russell O'Connor
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

Makefile

@@ -1,16 +1,16 @@
 all: Makefile.coq
-	+make -f Makefile.coq all
+	@+$(MAKE) -f Makefile.coq all
 
 clean: Makefile.coq
-	+make -f Makefile.coq clean
-	rm -f Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
-Makefile.coq: Make
-	$(COQBIN)coq_makefile -f Make -o Makefile.coq
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-Make: ;
+force _CoqProject Makefile: ;
 
-%: Makefile.coq
-	+make -f Makefile.coq $@
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: all clean
+.PHONY: all clean force

README.md

@@ -0,0 +1,66 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
+# Goedel
+
+[![Docker CI][docker-action-shield]][docker-action-link]
+[![Contributing][contributing-shield]][contributing-link]
+[![Code of Conduct][conduct-shield]][conduct-link]
+[![Zulip][zulip-shield]][zulip-link]
+
+[docker-action-shield]: https://github.com/coq-community/goedel/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/goedel/actions?query=workflow:"Docker%20CI"
+
+[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
+[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
+
+[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg
+[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md
+
+[zulip-shield]: https://img.shields.io/badge/chat-on%20zulip-%23c1272d.svg
+[zulip-link]: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users
+
+
+
+A proof in Coq of the Gödel-Rosser 1st incompleteness theorem,
+which says that any first order theory extending NN (which is PA
+without induction) that is complete is inconsistent.
+
+## Meta
+
+- Author(s):
+  - Russell O'Connor (initial)
+- Coq-community maintainer(s):
+  - Pierre Castéran ([**@Casteran**](https://github.com/Casteran))
+- License: [MIT License](LICENSE)
+- Compatible Coq versions: 8.7 or later
+- Additional dependencies:
+  - [Pocklington](https://github.com/coq-community/pocklington)
+- Coq namespace: `Goedel`
+- Related publication(s):
+  - [Essential Incompleteness of Arithmetic Verified by Coq](https://arxiv.org/abs/cs/0505034) doi:[10.1007/11541868_16](https://doi.org/10.1007/11541868_16)
+
+## Building and installation instructions
+
+The easiest way to install the latest released version of Goedel
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-goedel
+```
+
+To instead build and install manually, do:
+
+``` shell
+git clone https://github.com/coq-community/goedel.git
+cd goedel
+make   # or make -j <number-of-cores-on-your-machine> 
+make install
+```
+
+
+## Documentation
+
+More information about the project can be found at [this website](http://r6.ca/goedel1.html).

_CoqProject

@@ -0,0 +1,48 @@
+-R theories Goedel
+
+theories/checkPrf.v
+theories/chRem.v
+theories/codeFreeVar.v
+theories/codeList.v
+theories/codeNatToTerm.v
+theories/codePA.v
+theories/codeSubFormula.v
+theories/codeSubTerm.v
+theories/codeSysPrf.v
+theories/code.v
+theories/cPair.v
+theories/Deduction.v
+theories/expressible.v
+theories/extEqualNat.v
+theories/fixPoint.v
+theories/folLogic2.v
+theories/folLogic3.v
+theories/folLogic.v
+theories/folProof.v
+theories/folProp.v
+theories/folReplace.v
+theories/fol.v
+theories/goedel1.v
+theories/goedel2.v
+theories/Languages.v
+theories/ListExt.v
+theories/LNN2LNT.v
+theories/LNN.v
+theories/LNT.v
+theories/misc.v
+theories/model.v
+theories/NN2PA.v
+theories/NNtheory.v
+theories/NN.v
+theories/PAconsistent.v
+theories/PAtheory.v
+theories/PA.v
+theories/primRec.v
+theories/prLogic.v
+theories/PRrepresentable.v
+theories/rosserPA.v
+theories/rosser.v
+theories/subAll.v
+theories/subProp.v
+theories/wConsistent.v
+theories/wellFormed.v

coq-goedel.opam

@@ -0,0 +1,37 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "palmskog@gmail.com"
+version: "dev"
+
+homepage: "https://github.com/coq-community/goedel"
+dev-repo: "git+https://github.com/coq-community/goedel.git"
+bug-reports: "https://github.com/coq-community/goedel/issues"
+license: "MIT"
+
+synopsis: "Coq proof of the Gödel-Rosser 1st incompleteness theorem"
+description: """
+A proof in Coq of the Gödel-Rosser 1st incompleteness theorem,
+which says that any first order theory extending NN (which is PA
+without induction) that is complete is inconsistent."""
+
+build: ["dune" "build" "-p" name "-j" jobs]
+depends: [
+  "dune" {>= "2.5"}
+  "coq" {(>= "8.7" & < "8.14~") | (= "dev")}
+  "coq-pocklington" {= "dev"}
+]
+
+tags: [
+  "category:Mathematics/Logic/Foundations"
+  "keyword:goedel"
+  "keyword:rosser"
+  "keyword:incompleteness"
+  "keyword:logic"
+  "keyword:hilbert"
+  "logpath:Goedel"
+]
+authors: [
+  "Russell O'Connor"
+]

dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name goedel)