Skip to content

Commit

Permalink
[coq] Adapt to coq/coq#19530
Browse files Browse the repository at this point in the history
Note that:

- Coq is masking the `stdlib` directory in `dune`, using
  `(ignored_dirs ...)`
  • Loading branch information
ejgallego committed Dec 5, 2024
1 parent 5f386c9 commit 6648fdc
Show file tree
Hide file tree
Showing 4 changed files with 8 additions and 6 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@ jobs:
run: |
opam install lwt logs # Also build pet-server
opam install memprof-limits # We need to do this to avoid coq-lsp rebuilding Coq below due to deptops
opam install vendor/coq/{coq-core,coq-stdlib,coqide-server,coq}.opam
opam install vendor/coq/{coq-core,rocq-core,coq-stdlib,coqide-server,coq}.opam
- name: Install `coq-lsp` into OPAM switch
run: opam install .
Expand Down
8 changes: 5 additions & 3 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ COQ_BUILD_CONTEXT=../_build/default/coq

PKG_SET= \
vendor/coq/coq-core.install \
vendor/coq/coq-stdlib.install \
vendor/coq/rocq-core.install \
vendor/coq/stdlib/coq-stdlib.install \
coq-lsp.install

# Get the ocamlformat version from the .ocamlformat file
Expand Down Expand Up @@ -61,6 +62,7 @@ vendor/coq/config/coq_config.ml: vendor/coq
-libdir "$$EPATH/_build/install/default/lib/coq" \
-bytecode-compiler $(COQVM) \
-native-compiler no \
&& sed -i.bak 's/\((dirs .*\)/; \1/g' dune \
&& cp theories/dune.disabled theories/dune \
&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune

Expand All @@ -74,10 +76,10 @@ winconfig:
&& ./configure -no-ask -prefix "$$EPATH\\_build\\install\\default\\" \
-libdir "$$EPATH\\_build\\install\\default\\lib\\coq\\" \
-native-compiler no \
&& sed -i.bak 's/\((dirs .*\)/; \1/g' dune \
&& cp theories/dune.disabled theories/dune \
&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune


.PHONY: js
js: COQVM = no
js: coq_boot
Expand Down Expand Up @@ -144,7 +146,7 @@ make-fmt: build fmt
.PHONY: opam-update-and-reinstall
opam-update-and-reinstall:
git pull --recurse-submodules
for pkg in coq-core coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done
for pkg in coq-core rocq-core stdlib/coq-stdlib coqide-server coq; do opam install -y vendor/coq/$$pkg.opam; done
opam install .

.PHONY: patch-for-js
Expand Down
2 changes: 1 addition & 1 deletion coq/workspace.ml
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ let hash = Hashtbl.hash
let compare = Stdlib.compare

(* Lib setup, XXX unify with sysinit *)
let coq_root = Names.DirPath.make [ Libnames.coq_root ]
let coq_root = Names.DirPath.make [ Libnames.rocq_init_root ]
let default_root = Libnames.default_root_prefix

let mk_lp ~coq_path ~unix_path ~implicit =
Expand Down
2 changes: 1 addition & 1 deletion vendor/coq
Submodule coq updated 149 files

0 comments on commit 6648fdc

Please sign in to comment.