Stream: VsCoq devs & users

Topic: VsCoq weekly meeting


view this post on Zulip Maxime Dénès (Feb 08 2023 at 08:05):

Now that there's a very significant level of activity on VsCoq 2, we'd like to set up a VsCoq weekly meeting. We will mainly talk about VsCoq 2 dev, but also the maintenance of the current VsCoq if relevant. We need to find a convenient time slot, though. Would monday afternoon work? @Enrico Tassi @Romain Tetley @Hjalte Sorgenfrei Mac Dalland @Simon Green Kristensen @Laurent Théry @Huỳnh Trần Khanh @Paolo Giarrusso

view this post on Zulip Simon Green Kristensen (Feb 08 2023 at 08:15):

Tuesdays any time before 14:00 works better for @Hjalte Sorgenfrei Mac Dalland , @Jakob Israelsen and I.

view this post on Zulip Maxime Dénès (Feb 08 2023 at 08:32):

So what about Tuesdays at 10:00, is it ok for the other folks interested?

view this post on Zulip Enrico Tassi (Feb 08 2023 at 09:03):

OK for me as well

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 01:03):

Sorry, I fear I'll miss this week, but the timeslot's fine

view this post on Zulip Maxime Dénès (Feb 14 2023 at 07:27):

I posted some information for joining here: https://github.com/coq-community/vscoq/wiki/VsCoq-weekly-calls

view this post on Zulip Maxime Dénès (Feb 14 2023 at 07:27):

Feel to add topics if you want them to be discussed.

view this post on Zulip Karl Palmskog (Feb 14 2023 at 07:49):

this has probably been discussed already, but I worry a lot that we are going to experience even more fracturing in the Coq UI world going forward:

Is there a summary for us worriers what will/might happen?

view this post on Zulip Karl Palmskog (Feb 14 2023 at 07:54):

(I wouldn't have much to say in meetings, but am interested in outcomes)

view this post on Zulip Maxime Dénès (Feb 14 2023 at 08:11):

For VsCoq 1 & VsCoq 2, we are going to discuss it, but the plan will probably be something like maintaining both until the Coq versions supported by VsCoq 2 become old enough. Then phasing out VsCoq 1.

view this post on Zulip Maxime Dénès (Feb 14 2023 at 08:12):

The STM & XML protocol deprecation is fairly consensual too, AFAIK.

view this post on Zulip Pierre Roux (Feb 14 2023 at 08:23):

Karl Palmskog said:

Note that ProofGeneral is still using coqtop (not XML)

view this post on Zulip Hjalte Sorgenfrei Mac Dalland (Feb 14 2023 at 08:42):

Maybe it would be possibly to switch ProofGeneral over to vscoqtop when it matures with VsCoq2?

view this post on Zulip Théo Zimmermann (Feb 14 2023 at 09:41):

Coqtail is using the XML protocol. Once either vscoqtop or coq-lsp is considered mature enough, I think there should be an effort (coordinating UI maintainers and core devs) to migrate all the other widely used interfaces to use them. CoqIDE could then be either deprecated or migrated depending on what the long-term plan for it is (but as this stage, I believe that deprecating would be better, to avoid also having to handle other types of migrations, like to Gtk4).

view this post on Zulip Maxime Dénès (Feb 14 2023 at 10:16):

I added notes of the meeting (https://github.com/coq-community/vscoq/wiki/VsCoq-weekly-calls), thanks to all participants!

view this post on Zulip Wolf Honore (Feb 14 2023 at 13:04):

Théo Zimmermann said:

Coqtail is using the XML protocol.

There's been some preliminary discussion about moving Coqtail to coq-lsp: https://github.com/whonore/Coqtail/issues/7.

view this post on Zulip Paolo Giarrusso (Feb 14 2023 at 14:16):

relatedly to Proof General, does the vscoqtop roadmap already include replacing all PG/Company Coq features that they implement but shouldn't?

view this post on Zulip Paolo Giarrusso (Feb 14 2023 at 14:18):

Maxime Dénès said:

I added notes of the meeting (https://github.com/coq-community/vscoq/wiki/VsCoq-weekly-calls), thanks to all participants!

is there a workflow for issues affecting both, like https://github.com/coq-community/vscoq/issues/134 , or do we just do sth ad-hoc?

view this post on Zulip Laurent Théry (Feb 14 2023 at 14:20):

would be good to make an item list of all the features that are in the PG/ide/Vscoq and put a tick if there is an equivalent in the current vscoq2

view this post on Zulip Karl Palmskog (Feb 14 2023 at 14:21):

don't forget PG+CompanyCoq features in that case (not everyone uses CompanyCoq if they use PG)

view this post on Zulip Laurent Théry (Feb 14 2023 at 14:23):

what is the good tool to try to set up collaboratively this table?

view this post on Zulip Karl Palmskog (Feb 14 2023 at 14:28):

you could just use Markdown tables in the VsCoq wiki?

view this post on Zulip Laurent Théry (Feb 14 2023 at 15:27):

I've tried to do something. Not sure it is accurate/or exhaustive, feel free to edit it

view this post on Zulip Enrico Tassi (Feb 17 2023 at 16:31):

There was a request for a short intro to coq internals up to the proof/goals data structures. I plan to do it next Tuesday. Would that work?

view this post on Zulip Maxime Dénès (Feb 21 2023 at 13:19):

Did you guys have the short intro? If so, can you update https://github.com/coq-community/vscoq/wiki/VsCoq-weekly-calls to mention it?

view this post on Zulip Simon Green Kristensen (Feb 21 2023 at 13:19):

Yes, I'll update it

view this post on Zulip Maxime Dénès (Feb 21 2023 at 13:20):

(great, thanks ! And sorry, I'm on vacations ;) )

view this post on Zulip Maxime Dénès (Mar 07 2023 at 09:35):

I updated the wiki with notes from the meeting of today: https://github.com/coq-community/vscoq/wiki/VsCoq-weekly-calls

view this post on Zulip Maxime Dénès (Mar 14 2023 at 07:50):

We seem to have no specific topic to discuss today. Should we skip this occurrence of the call? Or are there last minute things to discuss?

view this post on Zulip Maxime Dénès (Mar 14 2023 at 07:53):

Cc @Enrico Tassi @Romain Tetley @Simon Green Kristensen @Hjalte Sorgenfrei Mac Dalland @Jakob Israelsen

view this post on Zulip Hjalte Sorgenfrei Mac Dalland (Mar 14 2023 at 07:56):

We dont have anything in particular, so it is fine with us if we skip it.

view this post on Zulip Romain Tetley (Mar 14 2023 at 08:04):

Nothing on my side either

view this post on Zulip Maxime Dénès (Mar 28 2023 at 06:52):

Hi there! Any last minute topic for this week's call?

view this post on Zulip Maxime Dénès (Mar 28 2023 at 06:53):

I don't have much to report on my side, still working on https://github.com/coq/coq/pull/17331. In particular, investigating the small slowdown and preparing more overlays for downstream developments.

view this post on Zulip Maxime Dénès (Mar 28 2023 at 06:54):

@Romain Tetley will be back with us next week, IIRC :)

view this post on Zulip Romain Tetley (Mar 28 2023 at 06:55):

I'm back but I'll be spectating this week :-)

view this post on Zulip Maxime Dénès (Mar 28 2023 at 06:56):

If no topics, let's skip this one.

view this post on Zulip Simon Green Kristensen (Mar 28 2023 at 07:07):

On our side, Hjalte is working on fixing state of sentences in the VSCoq document manager, Jakob is trying to unify types to make another heuristic, and I am making the test setup for testing our heuristics against each other via VSCode sorting and filtering of results

view this post on Zulip Jakob Israelsen (Mar 28 2023 at 07:12):

@Maxime Dénès I had a question, but I'll just ask it here: Do you have any suggestion on how we should checks if two types are able to unify? I found the unification module, which has w_unify, but that returns a evar_map which I am unsure of how to query for successful unification

view this post on Zulip Enrico Tassi (Mar 28 2023 at 08:21):

That is the old unification. Use Evarconv

view this post on Zulip Enrico Tassi (Mar 28 2023 at 08:22):

https://github.com/coq/coq/blob/9833a5160deb45e0750b40bb2e1a658071efa64e/pretyping/evarconv.mli#L56

view this post on Zulip Enrico Tassi (Mar 28 2023 at 08:23):

Unification is somewhat imperative, it assigns values to variables, and this state is carried by the evarmap.
If the terms are not unifiable, then evarconv raises an exception.

view this post on Zulip Enrico Tassi (Mar 28 2023 at 08:24):

The unify_flags will let you choose the degree of unfolding (less unfolding, faster runtime)

view this post on Zulip Jakob Israelsen (Mar 28 2023 at 08:25):

@Enrico Tassi Thanks, I'll give it a shot.

view this post on Zulip Jakob Israelsen (Mar 29 2023 at 12:45):

@Enrico Tassi I got unification to work, although it will only work if it solved the current goal. Is it also unification if my goal is B and I want to apply a lemma of type A -> B? Is that a flag in the unifcation I need to set, or is it another function entirely?

view this post on Zulip Enrico Tassi (Mar 29 2023 at 13:58):

I don't think there is a decent API for this, it is the job of the apply tactic to take a lemma f and try f, then f _, then f _ _ ...
This is what I use in srr: https://github.com/coq/coq/blob/master/plugins/ssr/ssrcommon.mli#L226 but you have to pass how many _ you want

view this post on Zulip Enrico Tassi (Mar 29 2023 at 13:58):

I mean, it is not incremental, but you can get started

view this post on Zulip Maxime Dénès (Apr 04 2023 at 07:01):

Enrico and Romain are not available this morning. @Jakob Israelsen @Hjalte Sorgenfrei Mac Dalland @Simon Green Kristensen any topics you'd like to discuss?

view this post on Zulip Hjalte Sorgenfrei Mac Dalland (Apr 04 2023 at 07:27):

We would like to discuss invalidation of state on the backend

view this post on Zulip Romain Tetley (Apr 18 2023 at 07:41):

Hi all,
Any special topics for today's call ? I don't have anything to report this week.

view this post on Zulip Notification Bot (Apr 18 2023 at 07:51):

A message was moved here from #VsCoq devs & users > VSCoq loading speed by Romain Tetley.

view this post on Zulip Hjalte Sorgenfrei Mac Dalland (Apr 18 2023 at 07:57):

We dont have anything

view this post on Zulip Simon Green Kristensen (Apr 18 2023 at 07:58):

We don't really have anything to talk about either

view this post on Zulip Maxime Dénès (Apr 18 2023 at 08:03):

I'm off this week ;)

view this post on Zulip Romain Tetley (Apr 18 2023 at 08:03):

cool let's cancel this one then ! see you next week ! ;-)

view this post on Zulip Maxime Dénès (Apr 25 2023 at 07:47):

Hi there! Any topics for this week? I was off last week so I don't have much. Did a bit of exploration of Rust Analyzer, semantic highlighting in LSP, nothing worth reporting yet.

view this post on Zulip Simon Green Kristensen (Apr 25 2023 at 08:00):

It is the last week we'll be working on code, as we are doing a code freeze on Friday.
(though we might need to work on testing, remains to be seen)

view this post on Zulip Maxime Dénès (Apr 25 2023 at 08:05):

So you plan to open a PR during the week?

view this post on Zulip Maxime Dénès (Apr 25 2023 at 08:05):

With completion ranking and the likes?

view this post on Zulip Simon Green Kristensen (Apr 25 2023 at 08:05):

no, not in that sense. We will need to decide which of the about 5 strategies makes the most sense to integrate into VSCoq

view this post on Zulip Simon Green Kristensen (Apr 25 2023 at 08:07):

Hjalte has some open PRs which you could look at, though. Attempts at speeding up VSCoq and fixing deletions.

view this post on Zulip Maxime Dénès (Apr 25 2023 at 08:08):

Yes, I'll look at them. We need to sync with @Romain Tetley , but the next step will surely be to consolidate the code & tests, so these patches will perfectly fit.

view this post on Zulip Maxime Dénès (Apr 25 2023 at 08:08):

Will you still be available next week, if you want to discuss the integration strategies?

view this post on Zulip Simon Green Kristensen (Apr 25 2023 at 08:09):

Sure, though what we can say will depend on tests of our strategies.

view this post on Zulip Maxime Dénès (Apr 25 2023 at 08:10):

Yes, so let's discuss after you've experimented

view this post on Zulip Enrico Tassi (May 02 2023 at 08:16):

We are a bit late today, the channel is now open but Romain and Maxime are not there yet

view this post on Zulip Enrico Tassi (May 02 2023 at 08:16):

Is anyone else going to join?

view this post on Zulip Maxime Dénès (May 09 2023 at 07:47):

Hi there! I'm travelling today, so won't be able to attend the call. @Enrico Tassi @Romain Tetley feel free to discuss any relevant topic, I'll catch up later.

view this post on Zulip Enrico Tassi (May 09 2023 at 08:23):

I'm busy with the math-comp 2.0 sprint


Last updated: Jun 23 2024 at 01:02 UTC