CohenCyril
commented
1 month ago FTR we used coq-elpi in Trocq which was based on HoTT and for which we plan to keep a HoTT option... I cannot remember a dependency on the prelude, where is it?
Open patrick-nicodemus opened 1 month ago
CohenCyril
commented
1 month ago FTR we used coq-elpi in Trocq which was based on HoTT and for which we plan to keep a HoTT option... I cannot remember a dependency on the prelude, where is it?
patrick-nicodemus
commented
1 month ago Yeah, I'm not exactly sure. All I know is that when I do From elpi Require Import elpi it loads the whole stdlib.
From elpi Require Import elpi.
(*
[Loading ML file ltac_plugin.cmxs (using legacy method) ...
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ...
[Loading ML file tauto_plugin.cmxs (using legacy method) ...
[Loading ML file cc_plugin.cmxs (using legacy method) ...
[Loading ML file firstorder_plugin.cmxs (using legacy method) ...
[Loading ML file ring_plugin.cmxs (using legacy method) ...
[Loading ML file coq-elpi.elpi ...
</infomsg> *)
Print Libraries.
Loaded library files:
Coq.Init.Notations
Coq.Init.Ltac
Coq.Init.Logic
Coq.Init.Datatypes
Coq.Init.Specif
Coq.Init.Decimal
Coq.Init.Hexadecimal
Coq.Init.Number
Coq.Init.Nat
Coq.Init.Byte
Coq.Init.Peano
Coq.Init.Wf
Coq.Init.Tactics
Coq.Init.Tauto
Coq.Init.Prelude
Coq.Classes.DecidableClass
Coq.Bool.Bool
Coq.Program.Basics
Coq.Classes.Init
Coq.Program.Tactics
Coq.Relations.Relation_Definitions
Coq.Classes.RelationClasses
Coq.Classes.Morphisms
Coq.Classes.CRelationClasses
Coq.Classes.CMorphisms
Coq.Classes.Morphisms_Prop
Coq.Classes.Equivalence
Coq.Classes.SetoidTactics
Coq.ssr.ssrclasses
Coq.ssr.ssrunder
Coq.ssr.ssrsetoid
Coq.Setoids.Setoid
Coq.Structures.Equalities
Coq.Relations.Relation_Operators
Coq.Relations.Operators_Properties
Coq.Relations.Relations
Coq.Structures.Orders
Coq.Numbers.NumPrelude
Coq.Structures.OrdersTac
Coq.Structures.OrdersFacts
Coq.Structures.GenericMinMax
Coq.Numbers.NatInt.NZAxioms
Coq.Numbers.NatInt.NZBase
Coq.Numbers.NatInt.NZAdd
Coq.Numbers.NatInt.NZMul
Coq.Logic.Decidable
Coq.Numbers.NatInt.NZOrder
Coq.Numbers.NatInt.NZAddOrder
Coq.Numbers.NatInt.NZMulOrder
Coq.Numbers.NatInt.NZParity
Coq.Numbers.NatInt.NZPow
Coq.Numbers.NatInt.NZSqrt
Coq.Numbers.NatInt.NZLog
Coq.Numbers.NatInt.NZDiv
Coq.Numbers.NatInt.NZGcd
Coq.Numbers.NatInt.NZBits
Coq.Numbers.Natural.Abstract.NAxioms
Coq.Numbers.NatInt.NZProperties
Coq.Numbers.Natural.Abstract.NBase
Coq.Numbers.Natural.Abstract.NAdd
Coq.Numbers.Natural.Abstract.NOrder
Coq.Numbers.Natural.Abstract.NAddOrder
Coq.Numbers.Natural.Abstract.NMulOrder
Coq.Numbers.Natural.Abstract.NSub
Coq.Numbers.Natural.Abstract.NMaxMin
Coq.Numbers.Natural.Abstract.NParity
Coq.Numbers.Natural.Abstract.NPow
Coq.Numbers.Natural.Abstract.NSqrt
Coq.Numbers.Natural.Abstract.NLog
Coq.Numbers.Natural.Abstract.NDiv
Coq.Numbers.Natural.Abstract.NDiv0
Coq.Numbers.Natural.Abstract.NGcd
Coq.Numbers.Natural.Abstract.NLcm
Coq.Numbers.Natural.Abstract.NLcm0
Coq.Numbers.Natural.Abstract.NBits
Coq.Numbers.Natural.Abstract.NProperties
Coq.Arith.PeanoNat
Coq.Arith.Factorial
Coq.Arith.Between
Coq.Logic.EqdepFacts
Coq.Logic.Eqdep_dec
Coq.Arith.Peano_dec
Coq.Arith.Compare_dec
Coq.Arith.EqNat
Coq.Arith.Wf_nat
Coq.Arith.Arith_base
Coq.Numbers.BinNums
Coq.PArith.BinPosDef
Coq.PArith.BinPos
Coq.NArith.BinNatDef
Coq.NArith.BinNat
Coq.PArith.Pnat
Coq.NArith.Nnat
Coq.setoid_ring.Ring_theory
Coq.Lists.List
Coq.setoid_ring.BinList
Coq.Numbers.Integer.Abstract.ZAxioms
Coq.Numbers.Integer.Abstract.ZBase
Coq.Numbers.Integer.Abstract.ZAdd
Coq.Numbers.Integer.Abstract.ZMul
Coq.Numbers.Integer.Abstract.ZLt
Coq.Numbers.Integer.Abstract.ZAddOrder
Coq.Numbers.Integer.Abstract.ZMulOrder
Coq.Numbers.Integer.Abstract.ZMaxMin
Coq.Numbers.Integer.Abstract.ZSgnAbs
Coq.Numbers.Integer.Abstract.ZParity
Coq.Numbers.Integer.Abstract.ZPow
Coq.Numbers.Integer.Abstract.ZDivTrunc
Coq.Numbers.Integer.Abstract.ZDivFloor
Coq.Numbers.Integer.Abstract.ZGcd
Coq.Numbers.Integer.Abstract.ZLcm
Coq.Numbers.Integer.Abstract.ZBits
Coq.Numbers.Integer.Abstract.ZProperties
Coq.ZArith.BinIntDef
Coq.ZArith.BinInt
Coq.setoid_ring.Ring_polynom
Coq.Lists.ListTactics
Coq.ZArith.Zeven
Coq.ZArith.Zcompare
Coq.ZArith.Zorder
Coq.Bool.Sumbool
Coq.ZArith.ZArith_dec
Coq.ZArith.Zbool
Coq.setoid_ring.InitialRing
Coq.setoid_ring.Ring_tac
Coq.setoid_ring.Ring_base
Coq.setoid_ring.Ring
Coq.setoid_ring.ArithRing
Coq.Arith.Arith
Coq.Strings.Byte
Coq.Strings.Ascii
Coq.Strings.String
elpi_elpi.dummy
Coq.Numbers.Cyclic.Abstract.CarryType
Coq.Numbers.Cyclic.Int63.PrimInt63
Coq.Floats.FloatClass
Coq.Floats.PrimFloat
elpi.elpiI think I used poor terminology. It "loads" the libraries, but does not import them.
So, in this case, all the names are qualified behind the full prefix Coq.Init.abc.
This is unlikely to cause a namespace collision accidentally.
Still, due to an unrelated bug with typeclass databases (https://github.com/coq/coq/issues/16934) as long as loading Elpi causes the prelude to be loaded, it will cause headaches trying to use Elpi in this setting.
patrick-nicodemus
commented
3 weeks ago I have investigated this issue and I think that this step in the build script is part of it.
https://github.com/LPCIC/coq-elpi/blob/2ef66b2640af1e3ef2e859f7b49b40d47272e10a/elpi/dune#L12
The String library loads a very surprising number of dependencies!
Require String.
[Loading ML file ltac_plugin.cmxs (using legacy method) ...
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ...
[Loading ML file tauto_plugin.cmxs (using legacy method) ...
[Loading ML file cc_plugin.cmxs (using legacy method) ...
[Loading ML file firstorder_plugin.cmxs (using legacy method) ...
[Loading ML file ring_plugin.cmxs (using legacy method) ...
</infomsg>The fact that the String module and all these plugins are imported into everyone that uses elpi via the dummy module elpi_elpi.dummy is unfortunate, would it be possible to change the build process so that a different way of tracking dependencies is used?
SkySkimmer
commented
3 weeks ago Those plugins are from the prelude, they are loaded by String because it doesn't use -noinit.
gares
commented
3 weeks ago That is a hack waiting for https://github.com/ocaml/dune/pull/9591 to be merged. Please ping the dune devs.
It would broaden the applicability of elpi if it could be used in projects compiled with the --no-init flag. I am interested in using Elpi in the Coq-HoTT library which does not use Prop anywhere and redefines equality to live in Type. Importing the stdlib is not itself fatal but one has to then be careful to avoid using any terms which are defined in the standard library.
Furthermore, if we import the stdlib it must be imported everywhere, which is annoying. It is currently not realistic/practical to import the stdlib only in the files that directly use Elpi due to a bug in the hint database system.