PG developer / maintainer telco

[hendriktews]

Hi,

a week ago I had a quite productive telco with @erikmd. We both thought that it might be a good idea to have a phone sync between people who contribute or contributed to PG. If you are interested, please drop a line here or send a message to me with the time zone you live in.

Hendrik

[cpitclaudel]

Sounds like a great idea, but my schedule is crazy these days :/ Let me know what you schedule and I'll see if I can join in (I'm on the east coast of the US)

[Matafou]

Next week should be ok for me. I am in Paris (GMT +1).

[erikmd]

Hi, I'm in Toulouse (Paris time = UTC+1); next week I'll only be available on {Wednesday−Thursday−Friday 12 February} (morning or after 18:30)

[hendriktews]

I believe, with the time difference, we can do between 15:00-18:00 CET (9:00-12:00 EST) or 20:00-23:00 CET (14:00-17:00 EST). Between 18:00 and 20:00 I have a daily priority family event. I created a poll with a few suggestions in that range in CW 9 and CW 10 at https://terminplaner4.dfn.de/ODlvvqfN5CSxcqxE . Please check with your calendar.

[erikmd]

@cpitclaudel https://terminplaner4.dfn.de/ODlvvqfN5CSxcqxE ← friendly ping :)

[cpitclaudel]

Sorry folks, I'm completely overbooked this for the next month :/ Can you keep me posted? :)

[hendriktews]

@erikmd @Matafou : How about Wednesday March 10 then? If it is fine with you I would propose to start at 21:00, otherwise we stay with 21:30. I can sent an invite for MS teams (runs in the native teams app and in chrome on linux or in edge), zoom (requires zoom) or nextcloud (runs in every browser AFAIK). Or do you prefer something else?

[erikmd]

Hi @hendriktews, March 10 @ 21:00 is OK for me.

Regarding the video system: I don't actually have the Zoom client installed on the workstation I usually develop for PG :) so my preferences would be 1. Nextcloud invitation link; otherwise 2. MS teams invitation link… You'll send this link by e-mail, won't you?

[Matafou]

March 10 21:00 CET. msteams or any browser-compatible is OK for me.

[hendriktews]

I've sent out the invitation by email.

[Matafou]

Do you have particular subjects in mind for this telco? I would like to hear your opinion on coq's xml protocol(s): mature enough? Should we give them a(nother) try? etc.

[hendriktews]

Pierre Courtieu [email protected] writes:

Do you have particular subjects in mind for this telco?

I though it would be good to share our priorities wrt. to Proof General. Maybe we can also get a little bit more organized wrt to announcing and open issues and pull requests.

I would like to hear your opinion on coq's xml protocol(s):

I never looked or tried that.

[erikmd]

I though it would be good to share our priorities wrt. to Proof General.

Indeed.

Also, we could discuss:

• some ideas regarding the documentation / discoverability of (new) PG features…
• as well as the discoverability of vanilla Emacs features themselves (notably to ease the Emacs learning curve for Coq users)

FTR, I recently gave a try to these 3 modes (mentioned in https://wikemacs.org/wiki/Discoverability) and they seem quite useful:

• https://melpa.org/#/helpful (requires Emacs 25)
• https://melpa.org/#/which-key (requires Emacs 24.4 so it's OK w.r.t. current PG requirements)
• https://melpa.org/#/discover-my-major

.emacs snippet − in case you'd like to try them as well!

(use-package helpful
  :ensure t
  :config
  (global-set-key (kbd "C-h f") #'helpful-callable)
  (global-set-key (kbd "C-h v") #'helpful-variable)
  (global-set-key (kbd "C-h k") #'helpful-key))

(use-package which-key
  :ensure t
  :config
  (which-key-mode))

(use-package discover-my-major
  :ensure t
  :config
  (global-set-key (kbd "C-h C-m") #'discover-my-major)
  (global-set-key (kbd "C-h M-m") #'discover-my-mode))

The first one, named "helpful", seems especially useful when developing/debugging Elisp code :) while the two other ones are more "general"… so maybe I'll add them to the .emacs template I prepared for my Coq course.

[erikmd]

Just to confirm @hendriktews @Matafou Cc @cpitclaudel, the next PG-dev-telco slot is scheduled on Wed. 14 Apr. 21:00 CEST (same place as before); and as we said last time, let's come each with some token to foster the discussion :) Cheers, − Erik

[hendriktews]

I confirm that I have topics to discuss and beer in the fridge. ;-)

[Matafou]

I'll be there. I would like to understand better how we can get rid of this "goal not showing" bugs. It must not be too difficult but PG architecture makes it a bit touchy. P.

Le mar. 13 avr. 2021 à 22:04, hendriktews @.***> a écrit :

I confirm that I have topics to discuss and beer in the fridge. ;-)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ProofGeneral/PG/issues/549#issuecomment-819017575, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFSL2VC6YJID5K6NINQ3D3TISPV3ANCNFSM4W3WRR6A .