From 356b92a3937ce69dbb6484bc0a8a35434398b4c8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Oct 2024 15:16:21 +0100 Subject: [PATCH 1/2] run all tests --- Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Makefile b/Makefile index 2a3cb1e66..0e027b7f7 100644 --- a/Makefile +++ b/Makefile @@ -18,6 +18,7 @@ build: test-core: $(call dune,runtest) tests + $(call dune,build) tests .PHONY: test-core test-apps: @@ -26,6 +27,7 @@ test-apps: test: $(call dune,runtest) + $(call dune,build) tests $(call dune,build) $$(find apps -type d -name tests) .PHONY: test From 2e8b4c7b8fde9c15ff43d10b390581a65f5ed9eb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Oct 2024 15:16:59 +0100 Subject: [PATCH 2/2] fix implementation of accumulation in the current library --- src/coq_elpi_programs.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index e3ea10d8c..e50c8a0e7 100644 --- a/src/coq_elpi_programs.ml +++ b/src/coq_elpi_programs.ml @@ -461,11 +461,21 @@ let get ?(fail_if_not_exists=false) p = { sources_rev = Chunk.Base { hash = hash_cunit base; base }; units = Names.KNset.singleton kname } | _ -> assert false + let is_inside_current_library kn = + Names.DirPath.equal + (Lib.library_dp ()) + (Names.KerName.modpath kn |> Names.ModPath.dp) + let in_db : Names.Id.t -> snippet -> Libobject.obj = let open Libobject in let cache ((_,kn),{ program = name; code = p; _ }) = db_name_src := SLMap.add name (append_to_db name kn p) !db_name_src in - let import i (_,s as o) = if Int.equal i 1 || s.scope = Coq_elpi_utils.SuperGlobal then cache o in + let load i ((_,kn),s as o) = + if Int.equal i 1 || + (s.scope = Coq_elpi_utils.Global && is_inside_current_library kn) || + s.scope = Coq_elpi_utils.SuperGlobal then cache o in + let import i (_,s as o) = + if Int.equal i 1 then cache o in declare_named_object @@ { (default_object "ELPI-DB") with classify_function = (fun { scope; program; _ } -> match scope with @@ -473,7 +483,7 @@ let get ?(fail_if_not_exists=false) p = | Coq_elpi_utils.Regular -> Substitute | Coq_elpi_utils.Global -> Keep | Coq_elpi_utils.SuperGlobal -> Keep); - load_function = import; + load_function = load; cache_function = cache; subst_function = (fun (_,o) -> o); open_function = simple_open import;