Skip to content

Computability: L -> MMA /\ MMA -> TM #176

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
yforster merged 7 commits into from
Nov 9, 2022
Merged

Computability: L -> MMA /\ MMA -> TM #176

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
80c29a4
shown L_computable -> MMA_computable, MMA_computable -> TM_computable
mrhaandi Sep 28, 2022
36f5898
removed redundant, complex L_computable_to_TM_computable proof
mrhaandi Oct 21, 2022
8b3f76d
removed smpl dependency
mrhaandi Oct 21, 2022
1478286
fixed CI
mrhaandi Oct 24, 2022
cd03959
typo
mrhaandi Nov 2, 2022
77653fa
removed superfluous List, Fin, Vector infrastructure
mrhaandi Nov 3, 2022
6c5c3b6
replaced complexity by computability
mrhaandi Nov 7, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ on: [push, pull_request]

env:
OCAML_VERSION: 4.11.0
CACHE_KEY: opam-8.16-${{github.base_ref}}-${{github.ref}}
CACHE_KEY: opam-8.16-${{github.base_ref}}-${{github.ref}}
jobs:
build-deps:
runs-on: ubuntu-latest
Expand Down
3 changes: 1 addition & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,14 +141,13 @@ opam pin add coq-library-undecidability.dev+8.16 "https://github.com/uds-psl/coq

### Manual installation (TENTATIVE)

You need `Coq 8.16` built on OCAML `>= 4.09.1`, the [Smpl](https://github.com/uds-psl/smpl) package and the Template-Coq (part of [MetaCoq](https://metacoq.github.io/)) package for Coq. If you are using opam 2 you can use the following commands to install the dependencies on a new switch:
You need `Coq 8.16` built on OCAML `>= 4.09.1`, and the Template-Coq (part of [MetaCoq](https://metacoq.github.io/)) package for Coq. If you are using opam 2 you can use the following commands to install the dependencies on a new switch:

```
opam switch create coq-library-undecidability --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda
eval $(opam env)
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq.8.16.dev
opam pin add -k git smpl.8.16 "https://github.com/uds-psl/smpl.git#coq-8.16"
opam pin add -k git coq-equations.1.3+8.16 "https://github.com/mattam82/Coq-Equations.git#8.16"
```

Expand Down
3 changes: 1 addition & 2 deletions opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,7 @@ install: [
depends: [
"coq" {= "8.16.0"}
"ocaml"
"coq-smpl" {>= "8.16"}
"coq-metacoq-template" {>= "1.1+8.16"}
"coq-metacoq-template" {>= "1.1.1+8.16"}
]

synopsis: "A Coq Library of Undecidability Proofs"
Expand Down
Loading