Maxime Dénès (Feb 08 2023 at 08:05): 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
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.
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?
Enrico Tassi (Feb 08 2023 at 09:03):OK for me as well
Paolo Giarrusso (Feb 13 2023 at 01:03):Sorry, I fear I'll miss this week, but the timeslot's fine
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
Maxime Dénès (Feb 14 2023 at 07:27):Feel to add topics if you want them to be discussed.
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?
Karl Palmskog (Feb 14 2023 at 07:54):(I wouldn't have much to say in meetings, but am interested in outcomes)
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.
Maxime Dénès (Feb 14 2023 at 08:12):The STM & XML protocol deprecation is fairly consensual too, AFAIK.
Pierre Roux (Feb 14 2023 at 08:23):Karl Palmskog said:
- STM and XML protocol deprecation, what happens to ProofGeneral
Note that ProofGeneral is still using coqtop (not XML)
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?
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).
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!
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.
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?
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?
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
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)
Laurent Théry (Feb 14 2023 at 14:23):what is the good tool to try to set up collaboratively this table?
Karl Palmskog (Feb 14 2023 at 14:28):you could just use Markdown tables in the VsCoq wiki?
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
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?
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?
Simon Green Kristensen (Feb 21 2023 at 13:19):Yes, I'll update it
Maxime Dénès (Feb 21 2023 at 13:20):(great, thanks ! And sorry, I'm on vacations ;) )
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
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?
Maxime Dénès (Mar 14 2023 at 07:53):Cc @Enrico Tassi @Romain Tetley @Simon Green Kristensen @Hjalte Sorgenfrei Mac Dalland @Jakob Israelsen
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.
Romain Tetley (Mar 14 2023 at 08:04):Nothing on my side either
Maxime Dénès (Mar 28 2023 at 06:52):Hi there! Any last minute topic for this week's call?
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.
Maxime Dénès (Mar 28 2023 at 06:54):@Romain Tetley will be back with us next week, IIRC :)
Romain Tetley (Mar 28 2023 at 06:55):I'm back but I'll be spectating this week :-)
Maxime Dénès (Mar 28 2023 at 06:56):If no topics, let's skip this one.
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
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
Enrico Tassi (Mar 28 2023 at 08:21):That is the old unification. Use Evarconv
Enrico Tassi (Mar 28 2023 at 08:22):https://github.com/coq/coq/blob/9833a5160deb45e0750b40bb2e1a658071efa64e/pretyping/evarconv.mli#L56
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.
Enrico Tassi (Mar 28 2023 at 08:24):The unify_flags will let you choose the degree of unfolding (less unfolding, faster runtime)
Jakob Israelsen (Mar 28 2023 at 08:25):@Enrico Tassi Thanks, I'll give it a shot.
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?
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
Enrico Tassi (Mar 29 2023 at 13:58):I mean, it is not incremental, but you can get started
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?
Hjalte Sorgenfrei Mac Dalland (Apr 04 2023 at 07:27):We would like to discuss invalidation of state on the backend
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.
Notification Bot (Apr 18 2023 at 07:51):A message was moved here from #VsCoq devs & users > VSCoq loading speed by Romain Tetley.
Hjalte Sorgenfrei Mac Dalland (Apr 18 2023 at 07:57):We dont have anything
Simon Green Kristensen (Apr 18 2023 at 07:58):We don't really have anything to talk about either
Maxime Dénès (Apr 18 2023 at 08:03):I'm off this week ;)
Romain Tetley (Apr 18 2023 at 08:03):cool let's cancel this one then ! see you next week ! ;-)
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.
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)
Maxime Dénès (Apr 25 2023 at 08:05):So you plan to open a PR during the week?
Maxime Dénès (Apr 25 2023 at 08:05):With completion ranking and the likes?
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
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.
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.
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?
Simon Green Kristensen (Apr 25 2023 at 08:09):Sure, though what we can say will depend on tests of our strategies.
Maxime Dénès (Apr 25 2023 at 08:10):Yes, so let's discuss after you've experimented
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
Enrico Tassi (May 02 2023 at 08:16):Is anyone else going to join?
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.
Enrico Tassi (May 09 2023 at 08:23):I'm busy with the math-comp 2.0 sprint
Last updated: Jun 04 2023 at 23:30 UTC