This gives the number of constants defined in Init
, not even including tactics:
~$ printf 'Search _.\n' | coqtop 2>/dev/null | grep '^[^ ]*:' | wc -l
989
This is way too much for things the user has absolutely no control on (except giving up on Init completely). IMHO, Init
should just include the bare minimum, for instance basic logical connectives, notations and a few well chosen basic tactics.
meh, it mostly looks reasonable to me
Out of curiosity, I tried the same thing in lean:
import Lean
#eval do
let env ← Lean.importModules #[{ module := `Init }] {}
println! env.constants.size
-- 23028
Lean's init is definitely not intended to be "just the bare minimum" though, and this count includes a lot of metaprogramming stuff and auxiliary definitions.
what about Core?
(Was that Q directed at me? I'll answer it anyway.) Lean core comes with two packages, Init
and Lean
, and there is also Std
which is a separate package but generally expected to be used (I think it's somewhat similar in scope to the coq standard library.) Doing that test, Init
has 23028 constants, Init + Lean
has 170004, and Init + Lean + Std
has 199570 constants. Lean is huge because it is the whole compiler, but large parts of it are also dependencies of code like Std because the API to elaboration and tactics is in Lean
so if you want to write metaprograms you usually need to depend on it (as I did in the test above, to be able to call Lean.importModules
).
Filtering out the definitions that are private or implementation-detail, and parsers and unexpanders, results in 5153 constants in Init
and paging through the results they seem to be mostly legitimate, although they still trend a bit towards internal details and generated functions from inductives and the like. Here's a random sampling:
#[SeqLeft.seqLeft, Nat.gcd_succ, Lean.ParserDescr.sepBy1, Trans.noConfusionType,
Lean.Meta.DSimp.Config.noConfusion, ReaderT.ext, Nat.Linear.Expr.of_cancel_lt, LawfulFunctor.comp_map,
Hashable.mk, HSub.mk, True.rec, IO.Prim.setAccessRights, Array.mk.inj, String.Iterator.atEnd,
Lean.Data.AC.Context.mk, Nat.Linear.Poly.denote_append, Lean.Parser.Category.doElem, Float.ofNat,
DoResultBC.casesOn, Lean.Meta.DSimp.Config.noConfusion, IO.monoMsNow, Substring.toIterator, Nonempty,
GetElem.rec, Repr.noConfusion]
source
(I'm going to be quiet now since this is probably a distraction from the question, which was about coq's init and not lean's. You can decide for yourself whether this should be taken as evidence that it's fine to have 1000 constants in init, or whether one ought to point and laugh at how bloated lean is.)
Thanks! This is relevant.
Noob question: what are "private" constants in Lean and why do they show up?
if you write private def foo := 1
then this is an actual definition which goes into the environment, but it has a name that can't be written outside the current file
Does it show up in searches?
no
the function I used, Name.isInternalDetail
, is generally used by user-facing tools to avoid giving results that can't be used
I want "private" in Coq, then :D
Doesn't coq have module privacy?
You can use modules for this, yes. But there is some boilerplate involved. Basically, you have to write a Module type and implement it with a Module.
How would that get counted in your test?
It's not used in Init.
Yes but it's more cumbersome to use:
Module Type FooS.
Parameter foo : ....
End FooS.
Module Import Foo : FooS
Definition bar := ...
Definition foo := ...
End Foo.
(* now only foo is visible (i.e. bar is private) *)
module abstraction will block computation though
ie if you do
private def foo := 1
def bar := foo + 1
in lean I imagine bar computes to 2
but using module abstraction to hide foo in Coq requires turning bar opaque
Module Type T. Parameter bar : nat. End T.
Module M : T. Definition foo := 1. Definition bar := foo + 1. End M.
Eval cbv in M.bar. (* = M.bar *)
there is also Local Definition which is closer to private but I guess Search doesn't respect it (https://github.com/coq/coq/issues/16949)
It's actually a bit complicated whether that will compute, there are different reducibility settings and one of them is opaque
which is basically the same as the opaqueness you get in coq. But it's true that privacy and reducibility are basically orthogonal concepts in lean
Pierre Rousselin said:
I want "private" in Coq, then :D
Isn't that what Local Definition
already does?
Stéphane Desarzens said:
Isn't that what
Local Definition
already does?
no, according to the refman,
Exception: when local is applied to Definition, Theorem or their variants, its semantics are different: it makes the defined objects available only through their fully qualified names rather than their unqualified names after an Import.
that's protected
in lean parlance
Last updated: Oct 13 2024 at 01:02 UTC