# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-num base Num library distributed with the OCaml compiler base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-perl 2 Virtual package relying on perl coq 8.6 Formal proof management system num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.03.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.03.0 Official 4.03.0 release ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.6 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "Hugo.Herbelin@inria.fr" homepage: "https://github.com/coq-contribs/intuitionistic-nuprl" license: "GPL" build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/IntuitionisticNuprl"] depends: [ "ocaml" "coq" {>= "8.6" & < "8.7~"} ] tags: [ "keyword: Nuprl" "keyword: computational type theory" "keyword: extensional type theory" "keyword: intuitionistic type theory" "keyword: Howe's computational equivalence relation" "keyword: Partial Equivalence Relation (PER) semantics" "keyword: consistency" "keyword: continuity" "keyword: bar induction" "category: Mathematics/Logic/Type theory" ] authors: [ "Vincent Rahli <vincent.rahli@gmail.com> [http://www.cs.cornell.edu/~rahli/]" "Abhishek Anand <abhishek.anand.iitg@gmail.com> [http://www.cs.cornell.edu/~aa755/]" "Mark Bickford <mark.concertina@gmail.com> [http://nuprl.org/]" ] bug-reports: "https://github.com/coq-contribs/intuitionistic-nuprl/issues" dev-repo: "git+https://github.com/coq-contribs/intuitionistic-nuprl.git" synopsis: "An Impredicative Model of Nuprl's Constructive Type Theory" description: """ http://www.nuprl.org/html/Nuprl2Coq/ This library formalizes Nuprl's Constructive Type Theory (CTT) as of 2015. CTT is an extensional type theory originally inspired by Martin-Lof's extensional type theory, and that has since then been extended with several new types such as: intersection types, union types, image types, partial types, set types, quotient types, partial equivalence relation (per) types, simulation and bisimulation types, an atom type, and the "Base" type. Our formalization includes a definition of Nuprl's computation system, a definition of Howe's computational equivalence relation and a proof that it is a congruence, an impredicative definition of Nuprl's type system using Allen's PER semantics (using Prop's impredicativity, we can formalize Nuprl's infinite hierarchy of universes), definitions of most (but not all) of Nuprl's inference rules and proofs that these rules are valid w.r.t. Allen's PER semantics, and a proof of Nuprl's consistency. In addition to the standard introduction and elimination rules for Nuprl's types, we have also proved several Brouwerian rules. Our computation system also contains: (1) free choice sequences that we used to prove Bar Induction rules; (2) named exceptions and a "fresh" operator to generate fresh names, that we used to prove a continuity rule. More information can be found here: http://www.nuprl.org/html/Nuprl2Coq/ Feel free to send questions to the authors or to nuprl@cs.cornell.edu""" flags: light-uninstall url { src: "https://github.com/coq-contribs/intuitionistic-nuprl/archive/v8.6.0.tar.gz" checksum: "md5=30ee492d77b04371c77c4266d0fe678e" }

- Command
`true`

- Return code
- 0

Dry install with the current Coq version:

- Command
`opam install -y --show-action coq-intuitionistic-nuprl.8.6.0 coq.8.6`

- Return code
- 0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

- Command
`true`

- Return code
- 0

- Command
`opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-intuitionistic-nuprl.8.6.0 coq.8.6`

- Return code
- 0
- Duration
- 1 m 0 s

- Command
`opam list; echo; ulimit -Sv 16000000; timeout 20h opam install -y -v coq-intuitionistic-nuprl.8.6.0 coq.8.6`

- Return code
- 0
- Duration
- 11 h 4 m

No files were installed.

- Command
`opam remove -y coq-intuitionistic-nuprl.8.6.0`

- Return code
- 0
- Missing removes
- none
- Wrong removes
- none