Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Include CoRN in the platform #31

Closed
VincentSe opened this issue Apr 9, 2020 · 9 comments
Closed

Include CoRN in the platform #31

VincentSe opened this issue Apr 9, 2020 · 9 comments

Comments

@VincentSe
Copy link

Description of the problem

Please include these 2 packages in both the windows installer and Coq platform
https://github.com/coq-community/corn
https://github.com/coq-community/math-classes

They contain the formalization of a large part of axiom-free constructive mathematics in Coq.

@Zimmi48
Copy link
Member

Zimmi48 commented Apr 9, 2020

Thanks @VincentSe for opening this issue. The Bignums add-on, on which Math-Classes (and thus CoRN) depend, is currently broken in the Windows installer, as reported here: coq-community/bignums#39.

So this issue will have to wait that this is fixed first. But it shouldn't be a problem for 8.12.

@Zimmi48
Copy link
Member

Zimmi48 commented May 12, 2020

@MSoegtropIMC Did you see this issue? Do you intend to look into it? If not, I could also take care of this.

@MSoegtropIMC
Copy link
Collaborator

It would definitely help, but I can also do it. I need to do a 8.12 prep day some time soon.

@Zimmi48 Zimmi48 self-assigned this May 12, 2020
@MSoegtropIMC
Copy link
Collaborator

@Zimmi48 : how do we handle this?

  • you do it
  • I do it
  • postpone to 8.12 platfor,m delivery?

@VincentSe : do you think it would be a problem to delay it to the 8.12 platform delivery, which should be about 4..6 weeks after the Coq release (also for 8.12+beta1).

@VincentSe
Copy link
Author

@MSoegtropIMC We can wait 6 weeks. Besides, depending on our meeting on Wednesday CoRN might be split into smaller packages.

@MSoegtropIMC
Copy link
Collaborator

@Zimmi48 : do you think it would be time to introduce a milestone 8.12+beta+platform? As I mentioned in a few PRs / issues my plan is to do a platform delivery for 8.12+beta and 8.12.0 in the intended timeframe (1..3 months) with a likely ETA of 4..6 weeks after the Coq core release - maybe some OSes will be available earlier or later.

@Zimmi48
Copy link
Member

Zimmi48 commented May 16, 2020

@MSoegtropIMC I'll simply remove the milestone and add this to the platform project for now. But eventually, we should create the platform repo in the Coq organization, and then we can migrate this issue there. I just want us to adjust the platform charter to better correspond to our shared vision before moving the repository in the official organization. (I will send you adjustment proposals ASAP.)

@MSoegtropIMC
Copy link
Collaborator

OK, I will keep a local list for the time being to track this. Please put a note to me in all issues which shall be addressed in the platform release. Something like:

@MSoegtropIMC : move to platform 8.12+beta

@Zimmi48 Zimmi48 transferred this issue from coq/coq Sep 19, 2020
@Zimmi48 Zimmi48 changed the title Please include CoRN and math-classes in Coq's windows installer Include CoRN in the platform Sep 30, 2020
@MSoegtropIMC
Copy link
Collaborator

Sorry for the long delay - fixed in #143.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants