Stream: Elpi users & devs

Topic: Inlining files containing `Elpi Accumulate File`

view this post on Zulip Jason Gross (May 24 2021 at 17:24):

My bug minimizer is incapable of inlining https://github.com/math-comp/hierarchy-builder/blob/master/structures.v into other files because Elpi Accumulate File is relative to ... the location from which coqc is called? So when I inline it into another file, the directive no longer points to a valid file. I'd like to have a way of adjusting Elpi Accumulate File which does not require parsing Coq files myself. The way that I handle this for Require is that I parse the .glob file, which will contain the line/character locations of all Require statements as well as the full logical path of the module being imported. Would it be possible to make Elpi Accumulate File emit a line into the .glob file (if it doesn't already) which contains the character locations of the file path string as well as the absolute path to the file, in a line like path ${start_byte_location}:${end_byte_location} '${absolute_path_to_file}' (or perhaps dir or dirpath or strpath or dirstring or similar in place of path)?

view this post on Zulip Jason Gross (May 24 2021 at 17:39):

(should I open an issue with this feature request?)

view this post on Zulip Enrico Tassi (May 24 2021 at 18:06):

As I hinted early, I don't think you should inline files that build elpi commands or tactics, like structures.v.
You should see them as .ml files which you cant just "require" via Declare ML Module (in the case of elpi would still be Require).
It that an option?

view this post on Zulip Jason Gross (May 24 2021 at 18:46):

Note that I'm not talking about inlining elpi directives into .v files, but talking about inlining .v files into other .v files. (This is analogous to inlining the Declare ML Module directive from one .v file into another, rather than trying to inline the .ml file into the .v file.)

view this post on Zulip Jason Gross (May 24 2021 at 18:48):

Assuming we're on the same page, what you say is an option, though if the dependency on the elpi commands/tactics is incidental and just packaged with the dependency, then the minimizer will be unable to see through the dependency.
In this case, the minimized .v file is

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hierarchy_builder/tests" "HB.tests" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hierarchy_builder/examples" "HB.examples" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hierarchy_builder" "HB" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/elpi" "elpi" "-top" "stage10") -*- *)
(* File reduced by coq-bug-finder from original input, then from 282 lines to 76 lines, then from 80 lines to 76 lines *)
(* coqc version 8.14+alpha compiled with OCaml 4.05.0
   coqtop version 8.14+alpha *)
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Require Coq.ZArith.ZArith.
Require HB.structures.
Import Coq.ssr.ssreflect.
Import Coq.ssr.ssrfun.
Import Coq.ZArith.ZArith.
Import HB.structures.

Declare Scope hb_scope.
Local Open Scope hb_scope.

HB.mixin Record AddAG_of_TYPE A := {
  zero : A;
  add : A -> A -> A;
  opp : A -> A;
  addrA : associative add;
  addrC : commutative add;
  add0r : left_id zero add;
  addNr : left_inverse zero opp add;
}.
HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.

Notation "0" := zero : hb_scope.
Infix "+" := (@add _) : hb_scope.
Notation "- x" := (@opp _ x) : hb_scope.
Notation "x - y" := (x + - y) : hb_scope.

Section AddAGTheory.
Variable A : AddAG.type.

Lemma addr0 : right_id (@zero A) add.
admit.
Defined.

Lemma addrK : right_loop (@opp A) (@add A).
admit.
Defined.

End AddAGTheory.
HB.factory Record Ring_of_TYPE A := {
  zero : A;
  one : A;
  add : A -> A -> A;
  opp : A -> A;
  mul : A -> A -> A;
  addrA : associative add;
  addrC : commutative add;
  add0r : left_id zero add;
  addNr : left_inverse zero opp add;
  mulrA : associative mul;
  mul1r : left_id one mul;
  mulr1 : right_id one mul;
  mulrDl : left_distributive mul add;
  mulrDr : right_distributive mul add;
}.

HB.builders Context A (a : Ring_of_TYPE A).

  HB.instance
  Definition to_AddAG_of_TYPE := AddAG_of_TYPE.Build A
    _ _ _ addrA addrC add0r addNr.

HB.end.

HB.instance Definition Z_ring_axioms :=
  Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul
    Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l
    Z.mul_assoc Z.mul_1_l Z.mul_1_r
    Z.mul_add_distr_r Z.mul_add_distr_l.

Example test1 (m n : Z) : (m + n) - n + 0 = m.
Proof.
by rewrite addrK addr0.

Perhaps this is as good as we can get with automatic minimization.

view this post on Zulip Enrico Tassi (May 25 2021 at 07:33):

I don't see much use of inlining the part of structures.v which defines HB.(mixin|structure|factory|builders|instance) and keep out of the picture HB.(about|graph|...). I mean, it would not help you.

On the contraty I think this file is pretty useful as is, since it minimizes the number of structures (in the HB sense) and builders and instances one needs in order to reproduce the problem. This will also be what one needs when mathcomp will use HB (currently in progress).

Last updated: Oct 13 2024 at 01:02 UTC