From 23448d1083dca8b8f24e65d9852ce8d4d21729c3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 11 May 2026 15:17:24 +0200 Subject: [PATCH 1/2] example for 407 --- tests/sources/bug_407.ml | 41 ++++++++++++++++++++++++++++++++++++++++ tests/sources/dune | 3 ++- tests/suite/elpi_api.ml | 5 +++++ 3 files changed, 48 insertions(+), 1 deletion(-) create mode 100644 tests/sources/bug_407.ml diff --git a/tests/sources/bug_407.ml b/tests/sources/bug_407.ml new file mode 100644 index 000000000..194f6d1f9 --- /dev/null +++ b/tests/sources/bug_407.ml @@ -0,0 +1,41 @@ +open Elpi.API + +let global = Ast.Loc.initial "init" +let base_str = + {| kind foo type. + external symbol mk_t : int -> foo = "1". + + type is_t foo -> int -> (pred). + is_t (mk_t N) N. + |} + +let is_t_c = RawData.Constants.declare_global_symbol "is_t" +let mk_t_c = RawData.Constants.declare_global_symbol "mk_t" +let query = + Ast.Term.mkAppGlobal ~loc:global ~hdloc:global is_t_c + (Ast.Term.mkVar ~loc:global ~hdloc:global (Ast.Name.from_string "X") []) + [Ast.Term.mkOpaque ~loc:global (RawOpaqueData.int.cino 4)] + +let () = begin + let flags = { Compile.default_flags with Compile.print_units = true } in + let elpi = Setup.init + ~builtins:[Elpi.Builtin.std_builtins] + ~flags:(Compile.to_setup_flags flags) + ~file_resolver:(Parse.std_resolver ~paths:[] ()) () in + let base = Parse.program_from ~elpi ~loc:global ~digest:(Digest.string "") (Lexing.from_string base_str) in + let pgm = Compile.program ~flags ~elpi base in + let query = Compile.optimize @@ RawQuery.compile_term pgm (fun st -> st, query) in + match Execute.once query with + | Execute.Success r -> + Setup.StrMap.iter begin fun k v -> + match RawData.look ~depth:0 v with + | RawData.App (c, _, _) -> + Format.printf "Solution: %a, %d, %d\n" + (Pp.term r.pp_ctx) v + c + mk_t_c; + assert(c == mk_t_c) + | _ -> exit 1 + end r.assignments + | _ -> exit 1 + end \ No newline at end of file diff --git a/tests/sources/dune b/tests/sources/dune index 36b3f659f..a0b6feccd 100644 --- a/tests/sources/dune +++ b/tests/sources/dune @@ -18,4 +18,5 @@ (executable (name sepcomp_tyid2) (modules sepcomp_tyid2) (libraries sepcomp)) (executable (name sepcomp_hover) (modules sepcomp_hover) (libraries sepcomp)) (executable (name sepcomp_extend_sig) (modules sepcomp_extend_sig) (libraries sepcomp)) -(executable (name sepcomp_extend_sig2) (modules sepcomp_extend_sig2) (libraries sepcomp)) \ No newline at end of file +(executable (name sepcomp_extend_sig2) (modules sepcomp_extend_sig2) (libraries sepcomp)) +(executable (name bug_407) (modules bug_407) (libraries elpi)) \ No newline at end of file diff --git a/tests/suite/elpi_api.ml b/tests/suite/elpi_api.ml index d8835f75d..bf6cb5232 100644 --- a/tests/suite/elpi_api.ml +++ b/tests/suite/elpi_api.ml @@ -83,3 +83,8 @@ let () = declare "sepcomp_extend_sig2" ~expectation:Test.Success () +let () = declare "bug_407" + ~source_dune:"bug_407.exe" + ~description:"misleading API" + ~expectation:Test.Success + () From 57a8f877973fd29225024d4fc32c3c73d42b023d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 11 May 2026 15:49:43 +0200 Subject: [PATCH 2/2] Update users.yml --- .github/workflows/users.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/users.yml b/.github/workflows/users.yml index 23a4fa0fe..c09ce143a 100644 --- a/.github/workflows/users.yml +++ b/.github/workflows/users.yml @@ -30,12 +30,12 @@ jobs: env: OPAMWITHTEST: false - - run: opam pin --ignore-constraints-on elpi add rocq-elpi https://github.com/LPCIC/coq-elpi.git#elpi-3.7 - - run: opam pin --ignore-constraints-on elpi add coq-elpi https://github.com/LPCIC/coq-elpi.git#elpi-3.7 + - run: opam pin --ignore-constraints-on elpi add rocq-elpi https://github.com/LPCIC/coq-elpi.git#master + - run: opam pin --ignore-constraints-on elpi add coq-elpi https://github.com/LPCIC/coq-elpi.git#master - run: opam pin --ignore-constraints-on elpi add rocq-stdlib https://github.com/rocq-prover/stdlib.git#master - run: opam pin --ignore-constraints-on elpi add coq-stdlib https://github.com/rocq-prover/stdlib.git#master - run: opam pin --ignore-constraints-on elpi,coq-stdlib add coq-trocq-std https://github.com/rocq-community/trocq.git#master - - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#hierarchy-builder.elpi-3.7 + - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#master - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-boot https://github.com/math-comp/math-comp.git#master - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-order https://github.com/math-comp/math-comp.git#master - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master