Stream: Coq devs & plugin devs

Topic: Init is too big


view this post on Zulip Pierre Rousselin (Dec 20 2023 at 14:41):

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.

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 14:43):

meh, it mostly looks reasonable to me

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:48):

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.

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 14:50):

what about Core?

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:00):

(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).

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:25):

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

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 15:26):

Thanks! This is relevant.

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 15:27):

Noob question: what are "private" constants in Lean and why do they show up?

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:28):

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

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 15:29):

Does it show up in searches?

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:29):

no

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:30):

the function I used, Name.isInternalDetail, is generally used by user-facing tools to avoid giving results that can't be used

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 15:31):

I want "private" in Coq, then :D

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:31):

Doesn't coq have module privacy?

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 15:32):

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.

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:33):

How would that get counted in your test?

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 15:33):

It's not used in Init.

view this post on Zulip Pierre Roux (Dec 20 2023 at 15:33):

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) *)

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 15:34):

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 *)

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 15:35):

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)

view this post on Zulip Mario Carneiro (Dec 20 2023 at 15:36):

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

view this post on Zulip Stéphane Desarzens (Dec 20 2023 at 21:30):

Pierre Rousselin said:

I want "private" in Coq, then :D

Isn't that what Local Definition already does?

view this post on Zulip Pierre Rousselin (Dec 21 2023 at 08:40):

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.

view this post on Zulip Mario Carneiro (Dec 21 2023 at 08:49):

that's protected in lean parlance


Last updated: Oct 13 2024 at 01:02 UTC