Commit f325817e authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Revert hack for coq 8.14 compilation.

Related issues:
- https://github.com/coq/coq/issues/15044 (bug report),
- https://github.com/ocaml/opam-repository/pull/19808 (package fix).
parent ddf48248
Pipeline #55677 failed with stage
in 9 minutes and 3 seconds
...@@ -6,7 +6,7 @@ stages: ...@@ -6,7 +6,7 @@ stages:
variables: variables:
# dune takes care of parallelization itself and does not like running in parallel # dune takes care of parallelization itself and does not like running in parallel
CPU_CORES: "1" CPU_CORES: "1"
MAKE_TARGET: "ci" MAKE_TARGET: "all_with_examples"
OCAML: "ocaml-base-compiler.4.07.1" OCAML: "ocaml-base-compiler.4.07.1"
.template: &template .template: &template
......
...@@ -6,10 +6,6 @@ all_with_examples: generate_all ...@@ -6,10 +6,6 @@ all_with_examples: generate_all
@dune build --display short @dune build --display short
.PHONY: all_with_examples .PHONY: all_with_examples
ci: restore_dune_project all_with_examples
@true
.PHONY: ci
install: install:
@dune install @dune install
.PHONY: install .PHONY: install
...@@ -41,18 +37,9 @@ clean: clean_generated ...@@ -41,18 +37,9 @@ clean: clean_generated
.PHONY: clean .PHONY: clean
builddep-opamfiles: builddep/refinedc-builddep.opam builddep-opamfiles: builddep/refinedc-builddep.opam
@echo "# Renaming dune-project to work around coq#15044"
@mv dune-project dune-project.tmp
@true @true
.PHONY: builddep-opamfiles .PHONY: builddep-opamfiles
restore_dune_project:
@if [ -f dune-project.tmp ] && ! [ -e dune-project ]; then \
echo "# Renaming dune-project back";\
mv dune-project.tmp dune-project;\
fi
.PHONY: restore_dune_project
# Create a virtual Opam package with the same deps as RefinedC, but no # Create a virtual Opam package with the same deps as RefinedC, but no
# build. Uses a very ugly hack to use sed for removing the last 4 # build. Uses a very ugly hack to use sed for removing the last 4
# lines since head -n -4 does not work on MacOS # lines since head -n -4 does not work on MacOS
...@@ -67,12 +54,8 @@ builddep/refinedc-builddep.opam: refinedc.opam Makefile ...@@ -67,12 +54,8 @@ builddep/refinedc-builddep.opam: refinedc.opam Makefile
# 2) they will remain satisfied even if other packages are updated/installed, # 2) they will remain satisfied even if other packages are updated/installed,
# 3) we do not have to pin the RefinedC package itself (which takes time). # 3) we do not have to pin the RefinedC package itself (which takes time).
builddep: builddep/refinedc-builddep.opam builddep: builddep/refinedc-builddep.opam
@echo "# Renaming dune-project to work around coq#15044"
@mv dune-project dune-project.tmp
@echo "# Installing package $^." @echo "# Installing package $^."
@opam install $(OPAMFLAGS) $^ @opam install $(OPAMFLAGS) $^
@echo "# Renaming dune-project back"
@mv dune-project.tmp dune-project
.PHONY: builddep .PHONY: builddep
# FIXME # FIXME
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment