ยซ Up

http dev Error ๐Ÿ”ฅ

๐Ÿ“… (2022-05-24 01:37:32 UTC)

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-gmp            4           Virtual package relying on a GMP lib system installation
coq                 dev         Formal proof management system
dune                3.1.1       Fast, portable, and opinionated build system
ocaml               4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2      Official release 4.10.2
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.9.3       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "Yishuai Li <yishuai@cis.upenn.edu>"
homepage: "https://github.com/liyishuai/coq-http"
dev-repo: "git+https://github.com/liyishuai/coq-http.git"
bug-reports: "https://github.com/liyishuai/coq-http/issues"
license: "MPL-2.0"
synopsis: "HTTP in Coq"
description: """
HTTP specification in Coq, testable and verifiable"""
build: [make "-j%{jobs}%" ]
run-test: [make "-j" jobs "test"]
install: [make "install" "INSTALLDIR=%{bin}%"]
depends: [
  "coq" { >= "8.13~" }
  "ocamlbuild" { >= "0.14.0" }
  "coq-quickchick"
  "coq-async-test"
]
tags: [
  "category:Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols"
  "category:Miscellaneous/Extracted Programs/Decision procedures"
  "keyword:co-induction"
  "keyword:extraction"
  "keyword:reactive systems"
  "logpath:HTTP"
]
authors: [
  "Yishuai Li <yishuai@cis.upenn.edu>"
  "Li-yao Xia <xialiyao@cis.upenn.edu>"
  "Yao Li <liyao@cis.upenn.edu>"
  "Azzam Althagafi <aazzam@cis.upenn.edu>"
  "Benjamin C. Pierce <bcpierce@cis.upenn.edu>"
]
url {
  src: "git+https://github.com/liyishuai/coq-http"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-http.dev coq.dev
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

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-http.dev coq.dev
Return code
0
Duration
27 m 59 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y coq-http.dev coq.dev
Return code
7936
Duration
9 m 30 s
Output
# Packages matching: installed
# Name                 # Installed # Synopsis
base-bigarray          base
base-threads           base
base-unix              base
conf-findutils         1           Virtual package relying on findutils
conf-gmp               4           Virtual package relying on a GMP lib system installation
coq                    dev         Formal proof management system
coq-async-test         dev         Testing asynchronous system
coq-ceres              dev         Library for serialization via S-expressions
coq-ext-lib            dev         a library of Coq definitions, theorems, and tactics
coq-itree              dev         A Library for Representing Recursive and Impure Programs in Coq
coq-itree-io           dev         Run interaction trees in IO
coq-json               dev         JSON in Coq
coq-mathcomp-ssreflect dev         Small Scale Reflection
coq-menhirlib          dev         A support library for verified Coq parsers produced by Menhir
coq-paco               dev         Coq library implementing parameterized coinduction
coq-parsec             dev         Monadic parser combinator library in Coq
coq-quickchick         dev         QuickChick is a random property-based testing library for Coq.
coq-simple-io          dev         IO monad for Coq
cppo                   1.6.8       Code preprocessor like cpp for OCaml
dune                   3.1.1       Fast, portable, and opinionated build system
menhir                 dev         An LR(1) parser generator
menhirLib              dev         Runtime support library for parsers generated by Menhir
menhirSdk              dev         Compile-time library for auxiliary tools related to Menhir
ocaml                  4.10.2      The OCaml compiler (virtual package)
ocaml-base-compiler    4.10.2      Official release 4.10.2
ocaml-config           1           OCaml Switch Configuration
ocamlbuild             0.14.1      OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind              1.9.3       A library manager for OCaml
zarith                 1.12        Implements arithmetic and logical operations over arbitrary-precision integers
[NOTE] Package coq is already installed (current version is dev).
The following actions will be performed:
  - install coq-http dev
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-http.dev] synchronised from git+https://github.com/liyishuai/coq-http
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq-http failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4".
#=== ERROR while compiling coq-http.dev =======================================#
# context              2.0.6 | linux/x86_64 | ocaml-base-compiler.4.10.2 | file:///home/bench/run/opam-coq-archive/extra-dev
# path                 ~/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-http.dev
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code            2
# env-file             ~/.opam/log/coq-http-31186-e4db2f.env
# output-file          ~/.opam/log/coq-http-31186-e4db2f.out
### output ###
# [...]
# COQC theories/Gen.v
# COQC theories/Tcp.v
# COQC theories/NetUnix.v
# COQC theories/Trace.v
# COQC theories/Observe.v
# File "./theories/Observe.v", line 37, characters 0-2077:
# Error: Stack overflow.
# 
# make[2]: *** [Makefile.coq:790: theories/Observe.vo] Error 1
# make[1]: *** [Makefile.coq:408: all] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.10.2/.opam-switch/build/coq-http.dev'
# make: *** [Makefile:9: coq] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-http dev
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none