imported from gitter room coq/stdlib2 · coq/stdlib2 devs

basically, in order to finish the new prelude, I need the coqlib patch to make tactics rebindable to new definitions of equality, logical connectors, etc

Gregory Malecha (Jul 19 2018 at 14:07):

i see

Maxime Dénès (Jul 19 2018 at 14:07):

that itself depends on some cleanups of the plugins

Gregory Malecha (Jul 19 2018 at 14:08):

is there a timeframe for that?

Maxime Dénès (Jul 19 2018 at 14:08):

like removing redundant plugins, to minimize the amount of work after that

Maxime Dénès (Jul 19 2018 at 14:08):

I think that part should be doable within two months

Gregory Malecha (Jul 19 2018 at 14:08):

weeks? months? years?

Gregory Malecha (Jul 19 2018 at 14:08):

Maxime Dénès (Jul 19 2018 at 14:08):

then there is another big task, which is to evaluate canonical structures vs typeclasses on large scale libraries

Maxime Dénès (Jul 19 2018 at 14:08):

so that we can make informed choices

Gregory Malecha (Jul 19 2018 at 14:09):

yeah....for that we need a canonical structures expert

Maxime Dénès (Jul 19 2018 at 14:09):

I have a few here, don't worry :)

Maxime Dénès (Jul 19 2018 at 14:09):

I even have two experts on canonical structures / typeclass comparison!

Maxime Dénès (Jul 19 2018 at 14:09):

but it is still very complex

Gregory Malecha (Jul 19 2018 at 14:09):

great

Gregory Malecha (Jul 19 2018 at 14:10):

i wonder if there is some way that we could get the best of both worlds

Maxime Dénès (Jul 19 2018 at 14:10):

after talking to them, the kind of experiments I would like to do is to take mathcomp and change a few basic constructions to typeclasses

Maxime Dénès (Jul 19 2018 at 14:10):

(like eqType typically)

Maxime Dénès (Jul 19 2018 at 14:10):

and see what happens

Maxime Dénès (Jul 19 2018 at 14:10):

if the whole thing can scale, etc

Gregory Malecha (Jul 19 2018 at 14:10):

ah, we are going to be doing something like that with the monads work (which has to be setoidy)

Maxime Dénès (Jul 19 2018 at 14:10):

also Enrico, Assia and Cyril did some work on compatibility layers

Maxime Dénès (Jul 19 2018 at 14:11):

so that's also valuable information, to know if interoperability between TC and CS works in practice

Maxime Dénès (Jul 19 2018 at 14:11):

once we have that, we can make sound design choices for the library

Maxime Dénès (Jul 19 2018 at 14:11):

unfortunately these questions have to be answered very early

Gregory Malecha (Jul 19 2018 at 14:11):

it seems like ideally you would want just 1

Maxime Dénès (Jul 19 2018 at 14:12):

yeah but even if the expressivity is equivalent, each choice has some impact on the packaging of structures, etc

Gregory Malecha (Jul 19 2018 at 14:12):

my understanding is that CS are fast and predicatble, and TC are slower and less predictable, but easier to program

Maxime Dénès (Jul 19 2018 at 14:12):

yeah but also for example: TC make you want to unbundle a lot of things, then you're missing support for first class contexts, etc

Maxime Dénès (Jul 19 2018 at 14:13):

on the other hand CS-based hierarchies are not easy to extend

Gregory Malecha (Jul 19 2018 at 14:13):

yes

Maxime Dénès (Jul 19 2018 at 14:13):

unfortunately, these questions are showing up as early as when defining structures with decidable equality

Maxime Dénès (Jul 19 2018 at 14:13):

and the experiments will take a few months again

Maxime Dénès (Jul 19 2018 at 14:14):

the good news is that I feel the system is making progress even during these preliminary steps

Gregory Malecha (Jul 19 2018 at 14:14):

so i'm wondering if it is possible to improve type classes (making them faster/more predictable) and add first-class contexts

Maxime Dénès (Jul 19 2018 at 14:14):

yeah my guess is that the conclusion of these experiments will be that none of the two mechanisms is perfect

Gregory Malecha (Jul 19 2018 at 14:14):

Maxime Dénès (Jul 19 2018 at 14:14):

and hopefully it will give a plausible candidate, that should be added a bit of infrastructure to cover all use cases

Maxime Dénès (Jul 19 2018 at 14:15):

I hope the plan makes sense

Gregory Malecha (Jul 19 2018 at 14:15):

it does

Maxime Dénès (Jul 19 2018 at 14:15):

this preliminary phase is the more tricky one to organize

Maxime Dénès (Jul 19 2018 at 14:15):

once it is done and the design choices are more stable, it is easier to share the work

Maxime Dénès (Jul 19 2018 at 14:16):

also, I'm working on another clean-up, whose first step is https://github.com/coq/coq/pull/8096

Maxime Dénès (Jul 19 2018 at 14:16):

the idea is to clarify the scoping of commands

Maxime Dénès (Jul 19 2018 at 14:16):

and the meaning of locality

Maxime Dénès (Jul 19 2018 at 14:17):

it has some impact on library design

Gregory Malecha (Jul 19 2018 at 14:17):

that would be really useful

Maxime Dénès (Jul 19 2018 at 14:17):

for example you can't really pack typeclasses in modules in a satisfactory way today

Gregory Malecha (Jul 19 2018 at 14:17):

selective import would be a huge win

Maxime Dénès (Jul 19 2018 at 14:17):

because the scoping is a bit wrong

Maxime Dénès (Jul 19 2018 at 14:17):

yes, exactly

Maxime Dénès (Jul 19 2018 at 14:17):

that typically avoids writing a lot of boilerplate

Maxime Dénès (Jul 19 2018 at 14:17):

with nested modules just to control the imports

Gregory Malecha (Jul 19 2018 at 14:18):

while your at it, a binary format that is independent of Ocaml serialization would be amazing :-)

Maxime Dénès (Jul 19 2018 at 14:18):

it did cross my mind ;)

Gregory Malecha (Jul 19 2018 at 14:18):

i'd be happy to hack on it with some pointers

Maxime Dénès (Jul 19 2018 at 14:18):

in fact I wonder if whitequark wasn't working on that

Gregory Malecha (Jul 19 2018 at 14:18):

Maxime Dénès (Jul 19 2018 at 14:18):

let me try to find it

Maxime Dénès (Jul 19 2018 at 14:19):

yeah I think it was part of https://github.com/coq/coq/issues/7839

Maxime Dénès (Jul 19 2018 at 14:20):

there's so much going on in the dev these days that it is hard to keep track even when working full time on it :)

Gregory Malecha (Jul 19 2018 at 14:22):

thanks @Maxime Dénès for the pointer

Maxime Dénès (Jul 19 2018 at 14:36):

@Théo Zimmermann I just configured the integration for this room, we'll see if it works

Théo Zimmermann (Jul 19 2018 at 14:36):

Your summary here is great @Maxime Dénès but I think you should also write it in a kind of roadmap in the stdlib2 repo to avoid getting these questions all the time.

Maxime Dénès (Jul 19 2018 at 14:36):

yes

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

I think the stdlib should be contained in one repostiory

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

even in the main coq one

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

however, it should be composed of quite a few modular components

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

we should be able to use a composable build

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

so modularity is assured

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

coq_dune should be able to handle that

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

I have a couple of things to discuss but I should submit the PR soon

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

the dune one is almost ready, I am finishing the doc up

Théo Zimmermann (Jul 19 2018 at 15:06):

I'm waiting for coq_dune like the messiah.

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

well there are some tricky parts yet

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

as like how to handle native compilation

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

also it is not clear to me how I should split the stdlib

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

I guess I will start with one directory = one (1) library

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

however it seems this is going to require quite a bit of reoganization

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

more than what we had to do for the ML files

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

so I dunno

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:08):

because in coq_dune, when you depend on (library coq.stdlib.zarith) you may not see list for example

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

also transitivity is interesting

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

anyways, I suggest to use a single repository

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

but structure it in a few smaller libraries

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

in fact, this is almost how ssreflect's is done

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

one file would basically be a single lib

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

ssr.nat

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:10):

well granularity is not easy

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:10):

we will see

Théo Zimmermann (Jul 19 2018 at 15:10):

Well you can maybe just keep the stdlib as one single package and experiment with finer grained modularity on stdlib2

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:12):

I'd prefer already to test the thing on live code

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

in fact, for example I want to put streams in coq.stdlib.streams-legacy

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

so people can migrate

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

hey by the way

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

how should we call the files?

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

in the future writing a dune file would suffice as coq_dune would be a pluging

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

but now we need a filename, maybe coqdune

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

coqproject

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

I dunno?

Théo Zimmermann (Jul 19 2018 at 15:14):

You mean it's a temporary name?

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

Once Dune understands .vo files hopefully we can deprecate them

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

this is not near

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

of course the old files would be supported for a while

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

the plugin would prefer them

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

and emit a warning

Théo Zimmermann (Jul 19 2018 at 15:15):

Is it supposed to subsume _CoqProject? Otherwise, do not call it coqproject.

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

yeah it is a bit different from coqproject

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

yeah let's call it coqdune

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

or coqlib

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

_CoqProject really has different functionality

Théo Zimmermann (Jul 19 2018 at 15:15):

:+1: on coqdune this is more explicit

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

merci

Emilio Jesús Gallego Arias (Jul 19 2018 at 15:19):

regarding coqdune coqfind, the main tricky part remaining is the bootstrap; in this setup, the stdlib is not special, coqdune just looks at what's on the tree and composes in the usual way; however there are a couple of tricky points to solve, they are not hard, but time consuming; a few other technical comments are on the issue but so far nobody gave feedback on them [like what's the proper layer for coqfind, etc...]

Emilio Jesús Gallego Arias (Jul 19 2018 at 16:17):

by the way @Théo Zimmermann the plan is that coqdune puts the vo files in a different directory, such as _build

Emilio Jesús Gallego Arias (Jul 19 2018 at 16:17):

and generates an install file

Emilio Jesús Gallego Arias (Jul 19 2018 at 16:17):

I guess that method is Ok for NiX, right?

Emilio Jesús Gallego Arias (Jul 19 2018 at 16:18):

proof general etc... will have to use the proper wrapper so paths are correctly set, as we do for merlin

Emilio Jesús Gallego Arias (Jul 19 2018 at 16:18):

tho CoqDune could generate _CoqProject files for compatiblity

Emilio Jesús Gallego Arias (Jul 19 2018 at 16:18):

I guess it is easy to teach PG about the current set of packages

Théo Zimmermann (Jul 19 2018 at 16:59):

Yes that's not a problem for nix. It's even better actually.

Emilio Jesús Gallego Arias (Jul 19 2018 at 20:02):

There are a few parts in coq that assume that v and go files are together. This may not be a problem but usually will add another delay...

Emilio Jesús Gallego Arias (Jul 19 2018 at 22:55):

Another question indeed I have [and maybe it is addressed but I didn't see it] is extraction and refinement

Emilio Jesús Gallego Arias (Jul 19 2018 at 22:55):

Including EAL-like refinement

Emilio Jesús Gallego Arias (Jul 19 2018 at 22:55):

this is common enough as to have standard structures

Bas Spitters (Jul 20 2018 at 13:28):

EAL refinement is interesting, there was a quest to combine it with https://github.com/parametricity-coq/paramcoq and the later work by Anand and Morrisett https://arxiv.org/abs/1705.01163

Théo Zimmermann (Jul 20 2018 at 13:30):

AFAIU Cyril Cohen has been struggling to find the right way to implement it. First using typeclasses, then paramcoq, and now Elpi.

Théo Zimmermann (Jul 20 2018 at 13:31):

So maybe not ready yet to be included in a "standard" library.

Bas Spitters (Jul 20 2018 at 13:31):

Regarding structures vs type classes has anyone looked at lean ? : https://leanprover.github.io/tutorial/

Chapter Structures.

They have a type class implementation, but provide some mechanisms for extending and renaming structures. It seems light weight, but the repackaging that is done behind the scenes looks really helpful and natural.

Théo Zimmermann (Jul 20 2018 at 13:33):

From what I know, Lean's author, Leonardo, has talked a lot to Georges Gonthier. So we can imagine that these additions were done following his feedback...

Bas Spitters (Jul 20 2018 at 13:35):

Yes, Leo has had a careful look at both ssr, but also math-classes, and seems to have found a good middle way. Maybe this is useful for Coq too.

Emilio Jesús Gallego Arias (Sep 11 2018 at 21:07):

Hi @Bas Spitters , certainly that seems like a very prioritary area for Coq Indeed.

Bas Spitters (Sep 12 2018 at 08:09):

We had a working group on algebraic structures in Dagstuhl. We are trying to write a conclusion of that https://www.dagstuhl.de/guestWiki/index.php/18341

Bas Spitters (Sep 12 2018 at 08:09):

@Cyril Cohen Was there too.

Emilio Jesús Gallego Arias (Sep 12 2018 at 10:52):

Thanks!

Bas Spitters (Jun 25 2019 at 11:31):

Related to this discussion about the future of the reals.
https://github.com/coq/coq/pull/9185
Is there an intended semantics for stdlib2? The classical set theoretical model, Propositions as Types, Propositions as Props, HoTT, ...

Théo Zimmermann (Jun 25 2019 at 15:52):

I don't want to speak for Maxime and Vincent, but I believe the goal is to stay in the setting that is most known (and not to invent anything really new): propositions as Props.

Bas Spitters (Jun 26 2019 at 08:09):

So... no real numbers in stdlib2 ?

Gregory Malecha (Jun 29 2019 at 02:52):

real numbers seem like a good library in and of their own right :-)

Bas Spitters (Mar 26 2020 at 07:26):

Any news from the coq call about stdlib2?

Maxime Dénès (Mar 26 2020 at 10:02):

we are working on integrating stdlib2's prelude, while still providing the old one for compatibility : https://github.com/coq/coq/pull/11747

Cyril Cohen (Apr 15 2020 at 14:08):

Hi, I am in the process of exporting gitter channels (public) data to zulip, (it can be done only once, during the creation of the zulip chatroom), do you wish that I export the data of this channel too?

Last updated: Oct 13 2024 at 01:02 UTC