Add giscus-based comments and reactions

[codrut3]

Add comment, votes and predictions features, based on giscus.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[mo271]

@zond can you have a look, since this is based on your original pr..

[mo271]

That looks great, thanks!

Perhaps we could add a documention/help page somewhere explaining the voting?!

EDIT

Especially so that users understand that votes are public and that a vote/comment is associated with their github user name

[zond]

Ah, sorry, completely missed this!

[zond]

Ah, sorry, completely missed this!

But it seems to have fairly little in common with my old PR :D

[Paul-Lez]

Looks good! One small question: is there a way to prevent users from voting simultaneously for "this conjecture is true" and for "this conjecture is false"?

[codrut3]

That looks great, thanks!

Perhaps we could add a documention/help page somewhere explaining the voting?!

Thank you for the suggestion, I added information in the About page, and linked to it from the theorem page.

[codrut3]

Looks good! One small question: is there a way to prevent users from voting simultaneously for "this conjecture is true" and for "this conjecture is false"?

I can probably hide the opposite emoji as long as the user stays in the tab, but if they reload the tab I'll lose the context. Should I look into this? @mo271

[mo271]

Looks good! One small question: is there a way to prevent users from voting simultaneously for "this conjecture is true" and for "this conjecture is false"?

I can probably hide the opposite emoji as long as the user stays in the tab, but if they reload the tab I'll lose the context. Should I look into this? @mo271

I think it is fine letting users upvote both True and False: perhaps we could even explain that this might correspond to "I think this question is not decidable/independent of ZFC" or something like that.
We can also do it in a follow up if we see that users are using it in this way

[mo271]

Thanks a lot, LTGM!