search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
198 stars 50 forks source link

ci: Add Coq dev #169

Closed liyishuai closed 4 years ago

liyishuai commented 4 years ago

Resolve #155

Removing upper bound on dependencies to include dev versions.

liyishuai commented 4 years ago

Compilation failed on Coq dev:

#=== ERROR while compiling coq-itree.dev ======================================#
# context     2.0.6 | linux/x86_64 | ocaml-base-compiler.4.05.0 | pinned(git+file:///home/coq/project#master#8286821e)
# path        ~/.opam/4.05.0/.opam-switch/build/coq-itree.dev
# command     /usr/bin/make -j2
# exit-code   2
# env-file    ~/.opam/log/coq-itree-2878-c743ac.env
# output-file ~/.opam/log/coq-itree-2878-c743ac.out
### output ###
# [...]
# COQC theories/Interp/InterpFacts.v
# COQC theories/Interp/RecursionFacts.v
# COQC theories/Simple.v
# COQC theories/Interp/HandlerFacts.v
# COQC theories/Events/StateFacts.v
# File "./theories/Interp/HandlerFacts.v", line 207, characters 0-442:
# Error: Cannot find an instance
# 
# make[2]: *** [Makefile.coq:715: theories/Interp/HandlerFacts.vo] Error 1
# make[1]: *** [Makefile.coq:339: all] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.05.0/.opam-switch/build/coq-itree.dev'
# make: *** [common.mk:6: coq] Error 2

Installed packages:

# Packages matching: installed
# Name                   # Installed # Synopsis
base-bigarray            base
base-num                 base        Num library distributed with the OCaml comp
base-threads             base
base-unix                base
conf-findutils           1           Virtual package relying on findutils
conf-m4                  1           Virtual package relying on m4
coq                      dev         pinned to version dev at git+https://github
coq-bignums              dev         Bignums, the Coq library of arbitrary large
coq-ext-lib              dev         a library of Coq definitions, theorems, and
coq-paco                 dev         Coq library implementing parameterized coin
dune                     2.4.0       pinned to version 2.4.0
num                      0           pinned to version 0
ocaml                    4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler      4.05.0      Official 4.05.0 release
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlbuild               0.14.0      OCamlbuild is a build system with builtin r
ocamlfind                1.8.1       pinned to version 1.8.1
ocamlfind-secondary      1.8.1       ocamlfind support for ocaml-secondary-compi
opam-depext              1.1.3       Query and install external dependencies of
Lysxia commented 4 years ago

Why does CI say this passed if dev failed?

liyishuai commented 4 years ago

Maybe it didn't report the status of dev to this PR.