From e964f5c5025093b949298fa1510f5e4c33368b53 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 9 Jul 2026 09:32:09 +0200 Subject: [PATCH] [rocq makefile] Don't erase ROCQPATH Fixing an unfortunate variable overlap from https://github.com/rocq-prover/rocq/pull/21564 --- tools/CoqMakefile.in | 10 +++++----- tools/rocqmakefile.ml | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 200c09a5d1c3..87b5fb59418d 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -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) @@ -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\ @@ -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; \ diff --git a/tools/rocqmakefile.ml b/tools/rocqmakefile.ml index 3acda768d96d..c943d773e357 100644 --- a/tools/rocqmakefile.ml +++ b/tools/rocqmakefile.ml @@ -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