Merge pull request #688 from proux01/stdlib_repo

Adapt to rocq-prover/rocq#19530

Author: gares

.nix/coq-overlays/coq-elpi/default.nix

@@ -10,7 +10,6 @@ let
     { case = "8.16"; out = { version = "1.17.0"; };}
     { case = "8.17"; out = { version = "1.17.0"; };}
     { case = "8.18"; out = { version = "1.18.1"; };}
-    { case = "8.19"; out = { version = "1.18.1"; };}
     { case = "8.20"; out = { version = "2.0.3"; };}
   ] {} );
 in (mkCoqDerivation {
@@ -78,6 +77,10 @@ in (mkCoqDerivation {
     maintainers = [ lib.maintainers.cohencyril ];
     license = lib.licenses.lgpl21Plus;
   };
+
+  preBuild = ''
+    make elpi/dune || true
+  '';
 }).overrideAttrs (o:
   lib.optionalAttrs (o.version != null
     && (o.version == "dev" || lib.versions.isGe "2.2.0" o.version))

Makefile

@@ -1,40 +1,50 @@
 dune = dune $(1) $(DUNE_$(1)_FLAGS)
 
-all:
+elpi/dune: elpi/dune.in
+	@rm -f $@
+	@echo "; generated by make, do not edit" > $@
+	@if $$(coqc --version | grep -q "8.19\|8.20") ; then \
+	  sed -e 's/@@STDLIB_THEORY@@//' $< >> $@ ; \
+	else \
+	  sed -e 's/@@STDLIB_THEORY@@/(theories Stdlib)/' $< >> $@ ; \
+	fi
+	@chmod a-w $@
+
+all: elpi/dune
 	$(call dune,build)
 	$(call dune,build) builtin-doc
 .PHONY: all
 
-build-core:
+build-core: elpi/dune
 	$(call dune,build) theories
 	$(call dune,build) builtin-doc
 .PHONY: build-core
 
-build-apps:
+build-apps: elpi/dune
 	$(call dune,build) $$(find apps -type d -name theories)
 .PHONY: build-apps
 
-build:
+build: elpi/dune
 	$(call dune,build) -p coq-elpi @install
 	$(call dune,build) builtin-doc
 .PHONY: build
 
-test-core:
+test-core: elpi/dune
 	$(call dune,runtest) tests
 	$(call dune,build) tests
 .PHONY: test-core
 
-test-apps:
+test-apps: elpi/dune
 	$(call dune,build) $$(find apps -type d -name tests)
 .PHONY: test-apps
 
-test:
+test: elpi/dune
 	$(call dune,runtest)
 	$(call dune,build) tests
 	$(call dune,build) $$(find apps -type d -name tests)
 .PHONY: test
 
-examples:
+examples: elpi/dune
 	$(call dune,build) examples
 .PHONY: examples
 
@@ -56,7 +66,7 @@ clean:
 	$(call dune,clean)
 .PHONY: clean
 
-install:
+install: elpi/dune
 	$(call dune,install) coq-elpi
 .PHONY: install
 

apps/tc/elpi/tc_aux.elpi

@@ -93,7 +93,7 @@ namespace tc {
     if (tc.is-option-active tc.oTC-clauseNameShortName)
       (Path = "")
       (coq.gref->path Gr [Hd | Tl], 
-        if (Hd = "Coq") (Hd' = "Stdlib") (Hd' = Hd),
+        if (Hd = "Coq") (Hd' = "Corelib") (Hd' = Hd),
         std.string.concat "." [Hd'|Tl] Path',
         Path is Path' ^ ".tc-"),
     % CAVEAT : Non-ascii caractars can't be part of a pred

apps/tc/tests/bigTest.v

@@ -882,7 +882,7 @@ instances *)
 Section prod_setoid.
   Context `{Equiv A, Equiv B}.
   Elpi Accumulate TC.Solver lp:{{
-    shorten tc-Stdlib.Classes.RelationClasses.{tc-Equivalence}.
+    shorten tc-Corelib.Classes.RelationClasses.{tc-Equivalence}.
     :after "lastHook"
     tc-Equivalence A RA R :-
       RA = {{@equiv _ (@prod_equiv _ _ _ _)}},
@@ -910,7 +910,7 @@ Section prod_setoid.
       std.map L1 remove_equiv_prod_equiv L2.
     remove_equiv_prod_equiv A A.
 
-    shorten tc-Stdlib.Classes.Morphisms.{tc-Proper}.
+    shorten tc-Corelib.Classes.Morphisms.{tc-Proper}.
 
     :after "lastHook" 
     tc-Proper A B C R :-
@@ -1043,7 +1043,7 @@ Elpi Accumulate TC.Solver lp:{{
       std.map L1 remove_equiv_sum_equiv L2.
     remove_equiv_sum_equiv A A.
 
-    shorten tc-Stdlib.Classes.Morphisms.{tc-Proper}.
+    shorten tc-Corelib.Classes.Morphisms.{tc-Proper}.
     :after "lastHook" 
     tc-Proper A B C R :-
       B = {{ @respectful _ _ _ _ }},

elpi/dune renamed to elpi/dune.in

@@ -1,6 +1,7 @@
 (coq.theory
  (name elpi_elpi) ; FIXME
- (package coq-elpi))
+ (package coq-elpi)
+ @@STDLIB_THEORY@@)
 
 (rule
  (target dummy.v)