(2019-04-07 12:48:26 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
coq 8.5.3 Formal proof management system.
num 0 The Num library for arbitrary-precision integer and ration
# opam file:
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
homepage: "https://github.com/lukaszcz/coqhammer"
dev-repo: "git+https://github.com/lukaszcz/coqhammer.git"
bug-reports: "https://github.com/lukaszcz/coqhammer/issues"
license: "LGPL 2.1"
build: [ make "-j%{jobs}%" ]
install: [ make "install" ]
remove: [
["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/Hammer'"]
["sh" "-c" "rm -f '%{bin}%/predict' '%{bin}%/htimeout'"]
]
depends: [
"ocaml"
"coq" {>= "8.7" & < "8.8~"}
]
tags: [ "keyword:automation"
"category:Misc/Coq Extensions"
"date:2018-04-09" ]
authors: [
"Lukasz Czajka <lukaszcz@mimuw.edu.pl>"
"Cezary Kaliszyk <cezary.kaliszyk@uibk.ac.at>"
"Burak Ekici <burak.ekici@uibk.ac.at>"
]
synopsis: "Automation for Dependent Type Theory"
url {
src: "https://github.com/lukaszcz/coqhammer/archive/v1.0.8-coq8.7.tar.gz"
checksum: "md5=01267d1ade74dd431ba15cee21c87217"
}
ruby lint.rb released opam-coq-archive/released/packages/coq-hammer/coq-hammer.1.0.8+8.7lint.rb:11:in `read': No such file or directory @ rb_sysopen - opam-coq-archive/released/packages/coq-hammer/coq-hammer.1.0.8+8.7/descr (Errno::ENOENT) from lint.rb:11:in `lint' from lint.rb:52:in `<main>'
Dry install with the current Coq version:
trueDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
truetruetrueNo files were installed.
true