hol-light icon indicating copy to clipboard operation
hol-light copied to clipboard

Published 20 hours ago • verified publisher icon jrh13

Forum for HOL Light questions, collaborations etc

Open brando90 opened this issue 5 years ago • 5 comments

What is the best way to communicate questions and collaborations for HOL Light?

For example Coq has:

  • discourse: https://coq.discourse.group/
  • gitter: https://gitter.im/ejgallego

Does HOL Light have something like this?

Or just stackoverflow?

brando90 avatar Oct 22 '19 20:10 brando90

The hol-info mailing list is a good place to ask questions for HOL Light (among other HOL systems).

PetrosPapapa avatar Oct 22 '19 21:10 PetrosPapapa

@PetrosPapapa why is there no discourse or gitter or slack or something like that?

Is it even worth asking in Stack Overflow for HOL Light?

brando90 avatar Oct 22 '19 21:10 brando90

@brando90 HOL Light is not as popular or as actively developed as Coq. I guess it's a small community and we are all used to the (over 20 year old) mailing list. People are quite responsive there though, and @jrh13 checks in periodically too, so it's worth trying.

PetrosPapapa avatar Oct 22 '19 22:10 PetrosPapapa

@PetrosPapapa is that the same list for HOL and HOL Light?

brando90 avatar Nov 08 '19 03:11 brando90

@PetrosPapapa is that the same list for HOL and HOL Light?

Yes, and for some other variants of the HOL prover actually.

maggesi avatar Nov 08 '19 13:11 maggesi