Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Nov 24 2020 10:46
    SkySkimmer commented #13464
  • Nov 24 2020 10:40
    herbelin commented #13460
  • Nov 24 2020 10:18
    jakobbotsch opened #13465
  • Nov 24 2020 10:18
    gares commented #13464
  • Nov 24 2020 10:12
    Zimmi48 updated the wiki
  • Nov 24 2020 10:11
    gares synchronize #13463
  • Nov 24 2020 10:10
    Zimmi48 updated the wiki
  • Nov 24 2020 10:05
    Zimmi48 commented #11390
  • Nov 24 2020 10:00
    herbelin commented #11390
  • Nov 24 2020 09:56
    Zimmi48 commented #11390
  • Nov 24 2020 09:52
    herbelin commented #11390
  • Nov 24 2020 09:46
    gares commented #13457
  • Nov 24 2020 09:46
    gares review_requested #13457
  • Nov 24 2020 09:46
    gares synchronize #13457
  • Nov 24 2020 09:43
    Zimmi48 assigned #13457
  • Nov 24 2020 09:38
    gares commented #13464
  • Nov 24 2020 09:36
    gares commented #13464
  • Nov 24 2020 09:35
    Zimmi48 commented #13449
  • Nov 24 2020 09:34
    gares commented #13464
  • Nov 24 2020 09:33
    gares commented #13464
Théo Zimmermann
@Zimmi48
BTW, are you aware that we've migrated our chat to Zulip? Cf. the message of @CohenCyril above (https://gitter.im/coq/coq?at=5ebeb020ecc55a312d050f75) on how to get back your account there.
Amin Timany
@amintimany
I am using 8.11.1. this was fixed after that?
Théo Zimmermann
@Zimmi48
Sorry, I read your comment too fast and was not clear in my answer. Yes, this is only in master and v8.12. The beta for 8.12 should be released soon.
Amin Timany
@amintimany
ok, thanks :-)
@Zimmi48 also, thanks for the heads up for Zulip, I sent a message to Cyril asking for access thre
Cyril Cohen
@CohenCyril
Dear gitter user,
if you posted at least one message in a Coq related gitter channel, your account has been ported to https://coq.zulipchat.com, with all the messages in your history. You have until June 5th 14:00 CEST to give me privately[*] an email associated with your github, gitlab or google account, in order for you to reclaim ownership.
After that we will archive your zulip account and if you want to log into zulip, you will have to create a fresh account.
Best wishes
[*] Please click on my picture, then "Chat Privately", then type: /me your-email-adress@yourprovider.org. This mail should be associated with a github, gitlab or even google account if you want to use one of these plateform to log in zulip
Cyril Cohen
@CohenCyril
@/all please read the above messages and take appropriate action
if you have not done it yet
Cyril Cohen
@CohenCyril
@jfehrle @urosn @cpitclaudel @amintimany @zunction @bollu, you have access to Coq zulip through "login with github/gitlab/google", at https://coq.zulipchat.com
Gaëtan Gilbert
@SkySkimmer
does anything bad happen if someone doesn't bother?
Théo Zimmermann
@Zimmi48

No, that's not a big deal. AFAICT, the only things you lose is:

  • your full sent message history (through Zulip, I can see all the messages I sent on Gitter)
  • the ability to edit the messages that you sent on Gitter (but given that those are pretty old, you normally don't need to do that)

And if someone does find some old message and want to talk to the person that sent them, they might reach out to the wrong account.

Cyril Cohen
@CohenCyril

And if someone does find some old message and want to talk to the person that sent them, they might reach out to the wrong account.

This last part is the most problematic, although when we will ask for old account to be archived, they will add a "(archived)" mention, so we can hope one would see it.

I also openned an issue on zulip to merge users zulip/zulip#14912, to be able to merge accounts after the fact, later on.

Also, every time one posts something here, I have to repost the announcement to move to zulip... so please refrain ;)
(otherwise it looses visibility)

Dear @/all
if you posted at least one message in a Coq related gitter channel, your account has been ported to https://coq.zulipchat.com, with all the messages in your history. You have until June 5th 14:00 CEST to give me privately[*] an email associated with your github, gitlab or google account, in order for you to reclaim ownership, if you did not do it yet.
After that we will archive your zulip account and if you want to log into zulip, you will have to create a fresh account.
Best wishes

[*] Please click on my picture, then "Chat Privately", then type: /me your-email-adress@yourprovider.org. This mail should be associated with a github, gitlab or even google account if you want to use one of these plateform to log in zulip

Hugo Herbelin
@herbelin

@Alizter:

Is there some way to define a mutual fixpoint with dependency?

I'd like to have recursion-recursion available too! @mattam82 had started a branch which includes recursion-recursion but he's pretty busy and probably needs help to finalize it.

Théo Zimmermann
@Zimmi48
In order to leave the message of @CohenCyril above regarding the move to Zulip very visible to all Gitter users, I am going to systematically remove all messages that get posted here after this one, until June 5th.
Cyril Cohen
@CohenCyril
@/all Reminder on June 5th 14:00 CEST, unless you already replied to me, you will not have the possibility to recover your automatically ported zulip account: it will be archived and you will have to create a new one to access https://coq.zulipchat.com. Please read my message above carefuly.
alexm98
@alexm98_gitlab
Hello everyone, I'm trying to run this function in Coq to see what it does, but I get "Unknown interpretation for :: ".
Fixpoint mistery (A : Type)(m : list bool)(s : list A) :=
match m, s with
| b :: m', x :: s' => if b then x :: mistery A m' s' else mistery A m' s'
| _, _ => nil
end.
Théo Zimmermann
@Zimmi48
@alexm98_gitlab Everyone has now moved to Zulip. I'd suggest you post your question there: https://coq.zulipchat.com/
alexm98
@alexm98_gitlab
Thank you @Zimmi48
YoungJu Song
@alxest
Hi,
I found that Coq introduced universe polymorphism in option/list types, but was reverted (https://github.com/coq/coq/blob/master/theories/Lists/List.v#L15, https://github.com/coq/coq/blob/master/theories/Init/Datatypes.v#L178).
What was the problem? Is there any plan to re-introduce universe polymorphism in the near future?
Théo Zimmermann
@Zimmi48
@alxest Everyone has now moved to Zulip. I'd suggest you post your question there: https://coq.zulipchat.com/ (more specifically in the Coq devs & plugin devs stream).
YoungJu Song
@alxest
Thanks a lot @Zimmi48 !
Cyril Cohen
@CohenCyril
Dear /@all good news, even if you did not migrate last May, you can now login on https://coq.zulipchat.com with your github account to reclaim ownership of the Zulip export of your gitter account on the Zulip Coq channels. After doing so, you may update your email.
However, if you did not follow the recommended procedure during the migration in May and opened a Zulip account on your own (and thus have two accounts on Coq's Zulip), you may run into problems. Please contact me if it happens.
Keigo Oka
@ogiekako
Hello. I'm a Coq newbie using https://github.com/coq-community/vscoq. It's quite good. However Format Document doesn't work. Is there a good auto formatter for coq usable from vscode?
Théo Zimmermann
@Zimmi48
Hi @ogiekako, this Gitter chat is closed. Please go to https://coq.zulipchat.com instead. There is a stream dedicated to vscoq over there.