Skip to content

Add a few operators to binrat (refinement of rat by bigQ) - #32

Merged
CohenCyril merged 7 commits into
rocq-community:masterfrom
proux01:binrat-div
Jan 18, 2021
Merged

Add a few operators to binrat (refinement of rat by bigQ)#32
CohenCyril merged 7 commits into
rocq-community:masterfrom
proux01:binrat-div

Conversation

@proux01

@proux01 proux01 commented Jan 8, 2021

Copy link
Copy Markdown
Collaborator

No description provided.

@proux01

proux01 commented Jan 18, 2021

Copy link
Copy Markdown
Collaborator Author

CI green, @CohenCyril would you allow me to merge this, do a release and the OPAM package or would you prefer to have a look first / do it yourself?

@CohenCyril
CohenCyril merged commit 5516a3a into rocq-community:master Jan 18, 2021
@CohenCyril

Copy link
Copy Markdown
Collaborator

@proux01 sure, you can go ahead.

@proux01
proux01 deleted the binrat-div branch January 18, 2021 17:12
@proux01

proux01 commented Jan 18, 2021

Copy link
Copy Markdown
Collaborator Author
  • I would be in favour of a transition to a meta.yml generated meta data.

good point, done

I'll be happy to try it once the required release of multinomials will have happened : math-comp/multinomials#38

@proux01

proux01 commented Jan 19, 2021

Copy link
Copy Markdown
Collaborator Author

So I just tried it, it's nice, a few minor comments:

  • I had to update from OPAM 2.0.3 to 2.0.5, an opam version check would be great, but definitely a detail
  • I had to git config --add github.user <user> otherwise the call to git config makes the whole script fail (on line 59, without error message, whatever the options provided)
  • I would love an option to use an already existing clone of coq-opam-archive, the clone takes both bandwidth and time

@CohenCyril

CohenCyril commented Jan 19, 2021

Copy link
Copy Markdown
Collaborator

Thank you very much for trying. Could you tell me what failed with opam 2.0.3?

@proux01

proux01 commented Jan 19, 2021

Copy link
Copy Markdown
Collaborator Author

The lint option check-upstream did not exist (it may exist in 2.0.4, haven't tried).

@CohenCyril

Copy link
Copy Markdown
Collaborator
  • I would love an option to use an already existing clone of coq-opam-archive, the clone takes both bandwidth and time

I will definitely provide this option. Note that you can also use --depth n (start with n=1 and increase if it does not work) to do a shallow clone (it may fail because sometimes pushes of branches from clones that are too shallow are rejected by github)

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants