(2019-11-30 21:22:11 UTC)
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq dev Formal proof management system
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.09.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.0 Official release 4.09.0
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "dev@clarus.me"
homepage: "https://github.com/clarus/coq-chick-blog"
dev-repo: "git+https://github.com/clarus/coq-chick-blog.git"
bug-reports: "https://github.com/clarus/coq-chick-blog/issues"
authors: ["Guillaume Claret"]
license: "MIT"
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
[make "-C" "extraction" "-j%{jobs}%"]
]
depends: [
"cohttp-lwt-unix"
"coq-error-handlers"
"coq-function-ninjas"
"coq-list-string"
"coq-moment"
"coq"
"lwt"
"ocaml"
"ocamlfind" {build}
]
tags: [
"date:2019-11-26"
"keyword:blog"
"keyword:effects"
"keyword:extraction"
]
synopsis: "A blog engine written and proven in Coq"
url {
src: "https://github.com/clarus/coq-chick-blog/archive/1.0.0.tar.gz"
checksum: "sha512=f54224caafc490f01896ff1fa1e6e9c71ff91ca5bf04fe00f4761dbd9e32758628f6be045b56f4a466574c05ae98edaf41931a1851ae59b8ab0686d83bb28036"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-chick-blog.1.0.0 coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-chick-blog.1.0.0 coq.devopam list; echo; ulimit -Sv 4000000; timeout 1h opam install -y -v coq-chick-blog.1.0.0 coq.dev# Packages matching: installed # Name # Installed # Synopsis astring 0.8.3 Alternative String module for OCaml base v0.12.2 Full standard library replacement for OCaml base-bigarray base base-bytes base Bytes library distributed with the OCaml compiler base-threads base base-unix base base64 3.2.0 Base64 encoding for OCaml cmdliner 1.0.4 Declarative definition of command line interfaces for OCaml cohttp 2.4.0 An OCaml library for HTTP clients and servers cohttp-lwt 2.4.0 CoHTTP implementation using the Lwt concurrency library cohttp-lwt-unix 2.4.0 CoHTTP implementation for Unix and Windows using Lwt conduit 2.0.2 A network connection establishment library conduit-lwt 2.0.2 A portable network connection establishment library using Lwt conduit-lwt-unix 2.0.2 A network connection establishment library for Lwt_unix conf-findutils 1 Virtual package relying on findutils conf-m4 1 Virtual package relying on m4 conf-ruby 1.0.0 Virtual package relying on Ruby coq dev Formal proof management system coq-cunit 1.0.0 Convenience functions for unit testing in Coq coq-error-handlers 1.2.0 Simple and robust error handling functions coq-function-ninjas 1.0.0 Simple functional combinators coq-list-plus 1.1.0 More functions on lists coq-list-string 2.1.2 Strings implemented as lists coq-moment 1.1.0 Parse, manipulate and pretty-print times and dates in Coq cppo 1.6.6 Code preprocessor like cpp for OCaml domain-name 0.3.0 RFC 1035 Internet domain names dune 2.0.0 Fast, portable, and opinionated build system dune-configurator 2.0.0 Helper library for gathering system configuration dune-private-libs 2.0.0 Private libraries of Dune fieldslib v0.12.0 Syntax extension to define first class values representing record fields, to get and set record fields, iterate and fold over all fields of a record and create new record values fmt 0.8.8 OCaml Format pretty-printer combinators ipaddr 4.0.0 A library for manipulation of IP (and MAC) address representations ipaddr-sexp 4.0.0 A library for manipulation of IP address representations usnig sexp jsonm 1.0.1 Non-blocking streaming JSON codec for OCaml logs 0.7.0 Logging infrastructure for OCaml lwt 4.4.0 Promises and event-driven I/O macaddr 4.0.0 A library for manipulation of MAC address representations magic-mime 1.1.2 Map filenames to common MIME types mmap 1.1.0 File mapping functionality num 1.3 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.09.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.0 Official release 4.09.0 ocaml-compiler-libs v0.12.1 OCaml compiler libraries repackaged ocaml-config 1 OCaml Switch Configuration ocaml-migrate-parsetree 1.5.0 Convert OCaml parsetrees between different versions ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects. ocamlfind 1.8.1 A library manager for OCaml ocplib-endian 1.0 Optimised functions to read and write int16/32/64 from strings and bigarrays, based on new primitives added in version 4.01. parsexp v0.12.0 S-expression parsing library ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_fields_conv v0.12.0 Generation of accessor and iteration functions for ocaml records ppx_sexp_conv v0.12.0 [@@deriving] plugin to generate S-expression conversion functions ppxlib 0.8.1 Base library and tools for ppx rewriters re 1.9.0 RE is a regular expression library for OCaml result 1.4 Compatibility Result module seq base Compatibility package for OCaml's standard iterator type starting from 4.07. sexplib v0.12.0 Library for serializing OCaml values to and from S-expressions sexplib0 v0.12.0 Library containing the definition of S-expressions and some base converters stdio v0.12.0 Standard IO library for OCaml stdlib-shims 0.1.0 Backport some of the new stdlib features to older compiler stringext 1.6.0 Extra string functions for OCaml topkg 1.0.1 The transitory OCaml software packager uchar 0.0.2 Compatibility library for OCaml's Uchar module uri 3.1.0 An RFC3986 URI/URL parsing library uri-sexp 3.1.0 An RFC3986 URI/URL parsing library uutf 1.0.2 Non-blocking streaming Unicode codec for OCaml [NOTE] Package coq is already installed (current version is dev). The following actions will be performed: - install coq-chick-blog 1.0.0 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-chick-blog.1.0.0: http] [coq-chick-blog.1.0.0] downloaded from https://github.com/clarus/coq-chick-blog/archive/1.0.0.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-chick-blog: ./configure.sh] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "./configure.sh" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-chick-blog.1.0.0) Processing 1/2: [coq-chick-blog: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-chick-blog.1.0.0) - COQDEP VFILES - COQC src/Model.v - COQC src/Http.v - File "./src/Model.v", line 70, characters 75-77: - Error: Expects a single character or a three-digits ascii code. - - COQC src/Request.v - Makefile:672: recipe for target 'src/Model.vo' failed - make[1]: *** [src/Model.vo] Error 1 - make[1]: *** Waiting for unfinished jobs.... - Makefile:326: recipe for target 'all' failed - make: *** [all] Error 2 [ERROR] The compilation of coq-chick-blog failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-chick-blog.1.0.0 ===============================# # context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.09.0 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.09.0/.opam-switch/build/coq-chick-blog.1.0.0 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-chick-blog-18231-2dea01.env # output-file ~/.opam/log/coq-chick-blog-18231-2dea01.out ### output ### # [...] # COQDEP VFILES # COQC src/Model.v # COQC src/Http.v # File "./src/Model.v", line 70, characters 75-77: # Error: Expects a single character or a three-digits ascii code. # # COQC src/Request.v # Makefile:672: recipe for target 'src/Model.vo' failed # make[1]: *** [src/Model.vo] Error 1 # make[1]: *** Waiting for unfinished jobs.... # Makefile:326: recipe for target 'all' failed # make: *** [all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-chick-blog 1.0.0 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-chick-blog.1.0.0 coq.dev' failed.
No files were installed.
true