Feature request: Remove dependence of elpi on stdlib

[patrick-nicodemus]

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.

[CohenCyril]

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]

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.elpi

[patrick-nicodemus]

I 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 (coq/coq#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]

I have investigated this issue and I think that this step in the build script is part of it.

coq-elpi/elpi/dune

Line 12 in 2ef66b2

(echo "Require Import String.\nOpen Scope string_scope.\nLocal Definition _hash := \"\n")

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]

Those plugins are from the prelude, they are loaded by String because it doesn't use -noinit.

[gares]

That is a hack waiting for ocaml/dune#9591 to be merged. Please ping the dune devs.