Skip to content

[rocq makefile] Don't erase ROCQPATH #22246

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 1 commit into from
Jul 9, 2026
Merged

[rocq makefile] Don't erase ROCQPATH #22246

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions tools/CoqMakefile.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ MLLIBFILES := $(COQMF_MLLIBFILES)
METAFILE := $(COQMF_METAFILE)
ROCQPACKAGE := $(COQMF_ROCQPACKAGE)
LEGACYSUPPORT := $(COQMF_LEGACY_SUPPORT)
HASROCQPATH := $(COQMF_HAS_ROCQPATH)
ROCQPATH := $(COQMF_ROCQPATH)
HAS_PACKAGE_LOGICAL_PATH := $(COQMF_HAS_PACKAGE_LOGICAL_PATH)
PACKAGE_LOGICAL_PATH := $(COQMF_PACKAGE_LOGICAL_PATH)
CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES)
INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
OTHERFLAGS := $(COQMF_OTHERFLAGS)
Expand Down Expand Up @@ -596,8 +596,8 @@ install: META
$(call findlib_remove)
$(call findlib_install, META $(FINDLIBFILESTOINSTALL))
$(HIDE)if [ "$(ROCQPACKAGE)" ]; then \
if [ "$(HASROCQPATH)" != "true" ]; then echo "Error: $(METAFILE) has no top-level rocqpath field"; exit 1; fi; \
root="$(subst .,/,$(ROCQPATH))"; \
if [ "$(HAS_PACKAGE_LOGICAL_PATH)" != "true" ]; then echo "Error: $(METAFILE) has no top-level rocqpath field"; exit 1; fi; \
root="$(subst .,/,$(PACKAGE_LOGICAL_PATH))"; \
for f in $$(cat .filestoinstall); do\
df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`"; rc="$$?";\
if [ "$$rc" != "0" -o -z "$$df" ]; then\
Expand All @@ -609,7 +609,7 @@ install: META
case "$$df" in \
"$$root") rel="" ;; \
"$$root"/*) rel="$${df#$$root/}" ;; \
*) echo SKIP "$$f" since it is outside rocqpath "$(ROCQPATH)"; continue ;; \
*) echo SKIP "$$f" since it is outside rocqpath "$(PACKAGE_LOGICAL_PATH)"; continue ;; \
esac; \
else \
case "$$rel" in /*) rel="$${rel#/}" ;; esac; \
Expand Down
4 changes: 2 additions & 2 deletions tools/rocqmakefile.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -435,8 +435,8 @@ let generate_conf_files oc p =
| Some _, Present x -> read_meta_rocqpath x
| _ -> None
in
fprintf oc "COQMF_HAS_ROCQPATH = %s\n" (if Option.has_some rocqpath then "true" else "false");
fprintf oc "COQMF_ROCQPATH = %s\n" (Option.default "" rocqpath)
fprintf oc "COQMF_HAS_PACKAGE_LOGICAL_PATH = %s\n" (if Option.has_some rocqpath then "true" else "false");
fprintf oc "COQMF_PACKAGE_LOGICAL_PATH = %s\n" (Option.default "" rocqpath)

let rec all_start_with prefix = function
| [] -> true
Expand Down
Loading