* (2019-04-07 14:40:39 UTC)*

# Installed packages for system: base-bigarray base Bigarray library distributed with the OCaml compiler base-num base Num library distributed with the OCaml compiler base-threads base Threads library distributed with the OCaml compiler base-unix base Unix library distributed with the OCaml compiler camlp5 7.06 Preprocessor-pretty-printer of OCaml conf-m4 1 Virtual package relying on m4 coq 8.6.1 Formal proof management system. num 0 The Num library for arbitrary-precision integer and ration ocamlfind 1.8.0 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
`ruby lint.rb released opam-coq-archive/released/packages/coq-intuitionistic-nuprl/coq-intuitionistic-nuprl.8.6.0`

- Return code
- 256
- Output
lint.rb:11:in `read': No such file or directory @ rb_sysopen - opam-coq-archive/released/packages/coq-intuitionistic-nuprl/coq-intuitionistic-nuprl.8.6.0/descr (Errno::ENOENT) from lint.rb:11:in `lint' from lint.rb:52:in `<main>'

Dry install with the current Coq version:

- Command
`true`

- 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
`true`

- Return code
- 0
- Duration
- 0 s

- Command
`true`

- Return code
- 0
- Duration
- 0 s

No files were installed.

- Command
`true`

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