Stream: coq/stdlib2 devs

Topic: imported from gitter room coq/stdlib2


view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:03):

Hi @Gregory Malecha ! Thanks for suggesting to create a room :)

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:03):

What's the status of everything right now @Maxime Dénès ?

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:04):

I'm updating the GitHub project so that it reflects the current status

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:04):

then I'll summarize here

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:04):

ok

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:05):

great. i'm starting some work to clean up and finish the ExtLib monad library

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:05):

i don't know if it belongs in stdlib2, but we'll see

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:06):

probably at least some parts, I guess

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:06):

i guess this is the question of monolithic repository vs small repositories

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:06):

so, if you look at https://github.com/orgs/coq/projects/1 you'll see the "in progress" and "infrastructure" columns

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:06):

it is still missing some things, but there is already a lot that is going on in terms of infrastructure

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:07):

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

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:07):

i see

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:07):

that itself depends on some cleanups of the plugins

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:08):

is there a timeframe for that?

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:08):

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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:08):

I think that part should be doable within two months

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:08):

weeks? months? years?

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:08):

ok

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:08):

so that we can make informed choices

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:09):

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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:09):

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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:09):

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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:09):

but it is still very complex

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:09):

great

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:10):

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

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:10):

(like eqType typically)

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:10):

and see what happens

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:10):

if the whole thing can scale, etc

view this post on Zulip 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)

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:10):

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

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:11):

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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:11):

unfortunately these questions have to be answered very early

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:11):

it seems like ideally you would want just 1

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:13):

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

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:13):

yes

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:13):

and the experiments will take a few months again

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:14):

ok

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:15):

I hope the plan makes sense

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:15):

it does

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:15):

this preliminary phase is the more tricky one to organize

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:16):

the idea is to clarify the scoping of commands

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:16):

and the meaning of locality

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:17):

it has some impact on library design

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:17):

that would be really useful

view this post on Zulip 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

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:17):

selective import would be a huge win

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:17):

because the scoping is a bit wrong

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:17):

yes, exactly

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:17):

that typically avoids writing a lot of boilerplate

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:17):

with nested modules just to control the imports

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:18):

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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:18):

it did cross my mind ;)

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:18):

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

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:18):

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

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:18):

oh

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:18):

let me try to find it

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:19):

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

view this post on Zulip 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 :)

view this post on Zulip Gregory Malecha (Jul 19 2018 at 14:22):

thanks @Maxime Dénès for the pointer

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Maxime Dénès (Jul 19 2018 at 14:36):

yes

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

I think the stdlib should be contained in one repostiory

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

even in the main coq one

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

we should be able to use a composable build

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:05):

so modularity is assured

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

coq_dune should be able to handle that

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

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

view this post on Zulip Théo Zimmermann (Jul 19 2018 at 15:06):

I'm waiting for coq_dune like the messiah.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

well there are some tricky parts yet

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:06):

as like how to handle native compilation

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

more than what we had to do for the ML files

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:07):

so I dunno

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

also transitivity is interesting

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

anyways, I suggest to use a single repository

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

but structure it in a few smaller libraries

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

one file would basically be a single lib

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:09):

ssr.nat

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:10):

well granularity is not easy

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:10):

we will see

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:12):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

so people can migrate

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

hey by the way

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:13):

how should we call the files?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

but now we need a filename, maybe coqdune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

coqproject

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

I dunno?

view this post on Zulip Théo Zimmermann (Jul 19 2018 at 15:14):

You mean it's a temporary name?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

Once Dune understands .vo files hopefully we can deprecate them

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

this is not near

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:14):

of course the old files would be supported for a while

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

the plugin would prefer them

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

and emit a warning

view this post on Zulip Théo Zimmermann (Jul 19 2018 at 15:15):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

yeah it is a bit different from coqproject

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

yeah let's call it coqdune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

or coqlib

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

_CoqProject really has different functionality

view this post on Zulip Théo Zimmermann (Jul 19 2018 at 15:15):

:+1: on coqdune this is more explicit

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 15:15):

merci

view this post on Zulip 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...]

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 16:17):

and generates an install file

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 16:17):

I guess that method is Ok for NiX, right?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 16:18):

tho CoqDune could generate _CoqProject files for compatiblity

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jul 19 2018 at 16:59):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 22:55):

Including EAL-like refinement

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2018 at 22:55):

this is common enough as to have standard structures

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 20 2018 at 13:31):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bas Spitters (Sep 12 2018 at 08:09):

@Cyril Cohen Was there too.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 12 2018 at 10:52):

Thanks!

view this post on Zulip 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, ...

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Jun 26 2019 at 08:09):

So... no real numbers in stdlib2 ?

view this post on Zulip Gregory Malecha (Jun 29 2019 at 02:52):

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

view this post on Zulip Bas Spitters (Mar 26 2020 at 07:26):

Any news from the coq call about stdlib2?

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 06:29 UTC