lpcic / coq-elpi Goto Github PK

and possibly the body, so that one can "clone" an abbreviation

Context: I want to prepare a patch for coq-elpi in view of a change on Coq's side.

I have a local Coq tree and I want to compile coq-elpi against it. The corresponding coqc is in the path, but when I run make, coq-elpi starts cloning Coq without asking me anything.

About installation, the README mentions only:

``
[blabla OPAM blabla]

You can also clone this repository and type make (in this case the plugin is compiled against the Coq version in the coq/ submodule directory).
``

Could you document how to build coq-elpi against a local tree? I had a brief look at the Makefile, but got lost in the hacks. It seems you rely on the location of the file produced by Coq's configure, for example. What is the point of all this? Superficially, it looks a bit like you are reimplementing some of the management of coq-elpi's dependencies in the Makefile...

Everyone can dream,... would it be possible one day to have

Elpi Command def.
Elpi Accumulate def lp:{{
main (arg-cons F (arg-decl X A Decl) :-
  pi x\ Decl x = arg-cons (str ":=") (arg-cons (trm (T x)) arg-nil)),
  Body = (fun X A x \ T),
  coq.env.typecheck Body _Ty,
  coq.env.add-const F Body _Ty ff ff _.
}}.
Elpi def f (x : bool) := x.
Check f.
(* f
	 : bool -> bool
*)

with

kind arguments type.
type arg-nil arguments.
type arg-cons argument -> arguments -> arguments.
type arg-binder name -> term -> (term -> arguments) -> arguments.

?

It is not possible to ask elpi to accumulate a clause to a database

I think the code of param1 and param2 should be ported to that API

CC @CohenCyril

Idea

{{ forall x (pp:X) : lp:T , lp:(B x) }}

to use X for the pretty printing hint of x.
Today you are forced to use prod X T x\B x to chose the pretty printing hint X

All combinators should use a solved? predicate to skip goals solved by side effect.

• export Elpi derive

Since what lives in env is already a gr

Behaving like [Global] Arguments foo : default implicits.

Please fix deprecation warnings for 8.9 so Elpi will be able to compile with 8.10, thanks!

File "src/coq_elpi_builtins.ml", line 571, characters 19-38:
Warning 3: deprecated: Check
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 575, characters 23-63:
Warning 3: deprecated: Enforce
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 575, characters 49-62:
Warning 3: deprecated: DefaultInline
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 625, characters 30-54:
Warning 3: deprecated: DefaultInline
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 638, characters 30-54:
Warning 3: deprecated: DefaultInline
Use the constructor in module [Declaremods]
CAMLC -c src/coq_elpi_vernacular.ml
File "src/coq_elpi_vernacular.ml", line 21, characters 0-50:
Warning 39: unused rec flag.
File "src/coq_elpi_builtins.ml", line 571, characters 19-38:
Warning 3: deprecated: Check
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 575, characters 23-63:
Warning 3: deprecated: Enforce
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 575, characters 49-62:
Warning 3: deprecated: DefaultInline
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 625, characters 30-54:
Warning 3: deprecated: DefaultInline
Use the constructor in module [Declaremods]
File "src/coq_elpi_builtins.ml", line 638, characters 30-54:
Warning 3: deprecated: DefaultInline
Use the constructor in module [Declaremods]
CAMLOPT -c -for-pack Elpi_plugin src/coq_elpi_vernacular.ml
File "src/coq_elpi_vernacular.ml", line 21, characters 0-50:
Warning 39: unused rec flag.

As of today every time you invoke an elpi command it is recompiled on the stop.
This is a waste of time, but more importantly makes {{ quotation }} see the state of Coq (eg open scopes).

Fixing this requires a proper separate compilation on the side of elpi (compile once in the Coq state the user expects), which has been on its way for some time, but is not there yet.

From elpi Require Import elpi.

Record test := Test {sort :> Type}.
Canonical can_test T := Test T.

Elpi Command test.
Elpi Query lp:{{
   coq.CS.db DB
}}.

gives

Error: Pattern matching failure embedding: cs-pattern: Default_cs

As a good example, do whd1 in all library function that do match on a type

currently we duplicate them, reusing only a few bits (field declaration), since the main entry points are not exported

As in hol light, use UnifVar in place of hole.
Beware coq.elab won't instantiate them, maybe...

This failed on HB generating an illtyped term:

(pi t\ coq.notation.abbreviation A [t] (X t),
print X % X = c\ a term

I have the following error message:

Using coq found in /nix/store/5hgy5hknybi927nillzb646ygwhw929i-coq-8.10+beta1/bin, from COQBIN or PATH
COQDEP VFILES
COQPP src/coq_elpi_vernacular_syntax.mlg
CAMLDEP src/coq_elpi_builtins.mli
CAMLDEP src/coq_elpi_goal_HOAS.mli
CAMLDEP src/coq_elpi_glob_quotation.mli
CAMLDEP src/coq_elpi_HOAS.mli
CAMLDEP src/coq_elpi_utils.mli
CAMLDEP src/coq_elpi_vernacular.mli
COQDEP src/elpi_plugin.mlpack
CAMLDEP src/coq_elpi_config.ml
CAMLDEP src/coq_elpi_builtins.ml
CAMLDEP src/coq_elpi_goal_HOAS.ml
CAMLDEP src/coq_elpi_glob_quotation.ml
CAMLDEP src/coq_elpi_name_quotation.ml
CAMLDEP src/coq_elpi_HOAS.ml
CAMLDEP src/coq_elpi_utils.ml
CAMLDEP src/coq_elpi_vernacular.ml
CAMLDEP src/coq_elpi_vernacular_syntax.ml
CAMLOPT -c -for-pack Elpi_plugin src/coq_elpi_config.ml
CAMLC -c src/coq_elpi_utils.mli
CAMLOPT -c -for-pack Elpi_plugin src/coq_elpi_utils.ml
CAMLC -c src/coq_elpi_HOAS.mli
CAMLOPT -c -for-pack Elpi_plugin src/coq_elpi_HOAS.ml
File "src/coq_elpi_HOAS.ml", line 222, characters 2-58:
Error (warning 32): unused value pp_elpi_evar.
File "src/coq_elpi_HOAS.ml", line 227, characters 4-17:
Error (warning 32): unused value empty.
File "src/coq_elpi_HOAS.ml", line 234, characters 4-42:
Error (warning 32): unused value pp.
File "src/coq_elpi_HOAS.ml", line 251, characters 2-60:
Error (warning 32): unused value pp_coq_engine.
File "src/coq_elpi_HOAS.ml", line 1670, characters 4-16:
Error (warning 32): unused value cc_constr2lp.
make[3]: *** [Makefile.coq:607: src/coq_elpi_HOAS.cmx] Error 2
make[2]: *** [Makefile.coq:321: all] Error 2
make[1]: *** [Makefile.coq:746: opt] Error 2
make: *** [Makefile:26: all] Error 2

using

$ coqtop -v
The Coq Proof Assistant, version 8.10+beta1 (May 2019)
compiled on May 20 2019 10:24:51 with OCaml 4.06.1

and I do not know how to print elpi version...

We currently use these 3 data types in the API

macro @gref :- ctype "Globnames.global_reference". % name for a global constant
macro @name :- ctype "Name.t".                     % name hint (compare as =)
string

I think we could add

macro @id :- ctype "Id.t"

and have all API adding things to the environment to require an @id, have conversion functions from the others to @id.

This new type could also be used in the module-related API, since @name is broken wrt comparison.

make it possible to Elpi foobar -> foobar

coq-elpi fails in newer OCaml version with

OCAMLOPT elpi_custom.cmx            -c
File "elpi_custom.ml", line 187, characters 32-33:
Error: This expression has type string but an expression was expected of type
         bytes

add a step to elpi.derive registering the CS for eqType (requires coq-mathcomp-ssreflect)

In addition to the tutorial it would be nice to provide examples such as:

• reification (example already in theories/tutorials/ by YB)
• DB population/retrieval
• ad-hoc proof search, eg the example in Beta's paper about CS
• clean up and document a couple of bricks in derive, eg "eq" and "param1"
• tactic to transfer the goal, eg bool-Prop, or maybe Zify
• quickchick generation of counter example

Elpi Command debug.
Elpi Query debug lp:{{
  coq.locate "bool" GR,
  coq.gr->string GR ID.
}}.

outputs

Query assignments:
  GR = indt «bool»
  ID = Coq.Init.Datatypes.bool.bool

Elpi foobar [ 33 | "ident" | ident | (term) | Record <record-syntax> ] .

print-ctx

Since we can't call the real elaborator, let's just remove this one.

In Coq there is no syntax to distinguish between Uniform and Non-Uniform parameters to Inductives. Coq infers it by their usage in the types of the constructor. This is not orthogonal to implicits, since an implicit status may make a parameter automatically inferred (as Uniform?).

This is too complex for Elpi's "inductive" argument, IMO, and also does not reflect how inductives are represented in Elpi: Uniform parameters do not occur as arguments to the inductivetype in the type of the constructors (they are fixed, why should you repeat them?), while Non-Uniform (and indexes) must appear (they vary, you must tell Elpi how). Coq-Elpi 1.3 only supports Record arguments, but I'd like to support also Inductive in 1.4 (to be released in few weeks).

I'm leaning toward imposing this very discipline for inductives used as arguments to Elpi commands.
Eg:

Elpi mycommand
  Inductive ty UP NuP : idx -> Type :=
  | K1 : ty (NuP * NuP) i -> ty NuP j
  | K2.

This also makes type checking of constructor with no given type for the conclusion (K2), it is
sufficient to unify they missing type with ty NuP _ (in this case the index is not inferrable, while the exact argument NuP is exactly what makes NuP a parameter and not an index, but that is the idea, I hope it is understandable).

This is not ideal, since one cannot just prefix any Coq Inductive declaration with, say, Elpi derive since he may had implicits on, or use @ and pass all arguments. But at the same time this design is very simple. The alternative is to have Elpi call the implicit argument machinery during the interning phase (note that Coq does intern + pretype inductive in a mixed way, so Elpi is already running its own code for inductives, since it has to stop after interning.. but so far this code is small, calling impargs does not not really thrill me).

Before committing to this design/compromise I'd love to hear from @maximedenes / @SkySkimmer since IIRC they did clean up a little inductive + implicits recently.

The given name is _elpi_ctx_entry_$n_

It is too simplistic

• may return duplicates
• does not shelve

https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder.20devs.20.26.20users/topic/Anomaly.20in.20kernel.2Fsafe_typing.2Eml

something is fishy when X = {{ let x : T := _ in x }} is run, in particular it seems no new evar constraint is generated for the body. It might be the code that detects progress in combination with some eager iota/beta reduction (also {{ (fun x : T => x) _ }} is problematic, while {{ f _ }} is OK).

it used to be there but got lost in a refactoring

Can we add parsing for arbitrary symbols so that
Elpi foo x := a.
has arguments [str ":=", str "a"] ?

An infixr declaration contained inside a Database seems to be applied to all subsequent Elpi tactics, regardless of whether that database was actually accumulated. This potentially makes typechecks successful even though the type was not correctly specified.