Cleanup after dropping 8.20

Author: proux01

.github/workflows/ci.yml

@@ -20,11 +20,10 @@ jobs:
           - 'rocq/rocq-prover:dev'
           - 'rocq/rocq-prover:9.1'
           - 'rocq/rocq-prover:9.0'
-          - 'coqorg/coq:8.20'
         profile:
           - dev
         include:
-          - image: 'coqorg/coq:8.20'
+          - image: 'rocq/rocq-prover:9.0'
             profile: fatalwarnings
       fail-fast: false  # don't stop jobs if one fails
     steps:

Makefile

@@ -1,59 +1,37 @@
 dune_wrap = $(shell command -v coqc > /dev/null || echo "etc/with-rocq-wrap.sh")
 dune = $(dune_wrap) dune $(1) $(DUNE_$(1)_FLAGS) --stop-on-first-error
-DUNE_IN_FILES = $(shell find . -name "dune.in" | sed -e 's/.in$$//')
 
 # This makefile is mostly calling dune and dune doesn't like
 # being called in parralel, so we enforce -j1
 .NOTPARALLEL:
 
-all: $(DUNE_IN_FILES)
+all:
 	$(call dune,build)
 	$(call dune,build) builtin-doc
 .PHONY: all
 
-# simplify this and get rid of the dune.in files once we require Rocq >= 9.0
-%dune: %dune.in
-	@rm -f $@
-	@echo "; generated by make, do not edit\n" > $@
-	@if test -e .coq-dune-files || \
-	    (command -v coqc > /dev/null && (coqc --version | grep -q '8.20')) ; then \
-	  sed -e 's/@@STDLIB_THEORY@@//' $< | \
-	  sed -e 's/@@STDLIB@@//' | \
-	  sed -e 's/@@ROCQ_RUNTIME@@/coq-core/g' >> $@ ; \
-	else \
-	  sed -e 's/@@STDLIB_THEORY@@/(theories Stdlib)/' $< | \
-	  sed -e 's/@@STDLIB@@/Stdlib/' | \
-	  sed -e 's/@@ROCQ_RUNTIME@@/rocq-runtime/g' >> $@ ; \
-	fi
-	@chmod a-w $@
-
-dune-files: $(DUNE_IN_FILES)
+dune-files:
+	echo "no longer doing anything"
 .PHONE: dune-files
 
-coq-dune-files:
-	touch .coq-dune-files
-	$(MAKE) dune-files
-	$(RM) .coq-dune-files
-.PHONE: coq-dune-files
-
-build-core: $(DUNE_IN_FILES)
+build-core:
 	$(call dune,build) theories
 	$(call dune,build) builtin-doc
 .PHONY: build-core
 
-build-apps: $(DUNE_IN_FILES)
+build-apps:
 	$(call dune,build) $$(find apps -type d -name theories)
 .PHONY: build-apps
 
-build: $(DUNE_IN_FILES)
+build:
 	$(call dune,build) -p rocq-elpi @install
 	$(call dune,build) builtin-doc
 .PHONY: build
 
 all-tests: test-core test-stdlib test-apps test-apps-stdlib
 .PHONY: all-tests
 
-test-core: $(DUNE_IN_FILES)
+test-core:
 	$(call dune,runtest) tests
 	$(call dune,build) tests
 	# Check for build reproducibility
@@ -65,22 +43,22 @@ test-core: $(DUNE_IN_FILES)
 	rm md5sum_accumulate1vo_1 md5sum_accumulate1vo_2
 .PHONY: test-core
 
-test-apps: $(DUNE_IN_FILES)
+test-apps:
 	$(call dune,build) $$(find apps -type d -name tests)
 .PHONY: test-apps
 
-test-apps-stdlib: $(DUNE_IN_FILES)
+test-apps-stdlib:
 	$(call dune,build) $$(find apps -type d -name tests-stdlib)
 .PHONY: test-apps-stdlib
 
-test-stdlib: $(DUNE_IN_FILES)
+test-stdlib:
 	$(call dune,build) tests-stdlib
 .PHONY: test-stdlib
 
 all-examples: examples examples-stdlib
 .PHONY: all-examples
 
-examples: $(DUNE_IN_FILES)
+examples:
 	$(call dune,build) examples
 .PHONY: examples
 
@@ -108,7 +86,7 @@ clean:
 	$(call dune,clean)
 .PHONY: clean
 
-install: $(DUNE_IN_FILES)
+install:
 	$(call dune,install) rocq-elpi
 .PHONY: install
 

README.md

@@ -1,5 +1,4 @@
 [![CI](https://github.com/LPCIC/coq-elpi/actions/workflows/ci.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/ci.yml)
-[![Nix 8.20](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-coq-8.20.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-coq-8.20.yml)
 [![Nix 9.0](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-rocq-9.0.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-rocq-9.0.yml)
 [![Nix 9.1](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-rocq-9.1.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-rocq-9.1.yml)
 [![Nix master](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-coq-master.yml/badge.svg)](https://github.com/LPCIC/coq-elpi/actions/workflows/nix-action-coq-master.yml)

_CoqProject

@@ -10,8 +10,6 @@
 
 -R theories elpi
 -R _build/default/theories elpi
--Q theories-stdlib elpi_stdlib
--Q _build/default/theories-stdlib elpi_stdlib
 
 -Q elpi elpi_elpi
 -Q _build/default/elpi elpi_elpi

apps/coercion/src/dune.in renamed to apps/coercion/src/dune

@@ -3,7 +3,7 @@
  (public_name rocq-elpi.coercion)
  (flags :standard -w -27)
  (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
- (libraries @@ROCQ_RUNTIME@@.plugins.ltac @@ROCQ_RUNTIME@@.vernac rocq-elpi.elpi))
+ (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi))
 
 (coq.pp
  (modules rocq_elpi_coercion_hook))

apps/coercion/tests/test_open.v

@@ -1,5 +1,5 @@
 From elpi.apps Require Import coercion.
-From elpi.core Require Import ssreflect.
+From Corelib Require Import ssreflect.
 
 Ltac my_solver := try ((repeat apply: le_n_S); apply: le_0_n).
 

apps/cs/src/dune.in renamed to apps/cs/src/dune

@@ -3,7 +3,7 @@
  (public_name rocq-elpi.cs)
  (flags :standard -w -27)
  (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
- (libraries @@ROCQ_RUNTIME@@.plugins.ltac @@ROCQ_RUNTIME@@.vernac rocq-elpi.elpi))
+ (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi))
 
 (coq.pp
  (modules rocq_elpi_cs_hook))

apps/cs/src/rocq_elpi_cs_hook.mlg

@@ -7,7 +7,7 @@ open Elpi_plugin
 open Rocq_elpi_arg_syntax
 open Rocq_elpi_vernacular
 
-[%%if coq = "8.20" || coq = "9.0" || coq = "9.1"]
+[%%if coq = "9.0" || coq = "9.1"]
 let structure_projection_nparams env ind = Structures.Structure.projection_nparams ind
 [%%else]
 let structure_projection_nparams env ind = Structures.Structure.projection_nparams env ind
@@ -65,20 +65,14 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
 		 | API.Execute.Failure -> None
 		 end
 
-[%%if coq = "8.20"]
-let adapt_hook f : Evarconv.hook = fun env sigma (s,l,t) x -> f env sigma (s,Some l,t) x
-[%%else]
-let adapt_hook f : Evarconv.hook = f
-[%%endif]
-
 let add_cs_hook =
   let cs_hook_program = Summary.ref ~name:"elpi-cs" None in
   let cs_hook env sigma proj pat =
     match !cs_hook_program with
     | None -> None
     | Some h -> elpi_cs_hook h env sigma proj pat in
   let name = "elpi-cs" in
-  Evarconv.register_hook ~name (adapt_hook cs_hook);
+  Evarconv.register_hook ~name cs_hook;
   let inCs =
     let cache program =
       cs_hook_program := Some program;

apps/derive/tests-stdlib/dune

@@ -2,6 +2,6 @@
  (package rocq-elpi-tests-stdlib)
  (name elpi_apps_derive_tests_stdlib)
  (flags :standard -w -default-output-directory)
- (theories elpi elpi.apps.derive elpi.apps.derive.tests elpi_stdlib))
+ (theories elpi elpi.apps.derive elpi.apps.derive.tests Stdlib))
 
 (include_subdirs qualified)

apps/derive/tests/test_bcongr.v

@@ -1,4 +1,3 @@
-From elpi.core Require Import Bool.
 From elpi.apps Require Import derive.bcongr.
 
 From elpi.apps Require Import test_derive_corelib test_projK.