Use of "pipe" function is not (easily) Windows compatible about coqprime HOT 24 CLOSED

@MSoegtropIMC Great ! I have updated the release. Should be ok now.

from coqprime.

Should a Windows (and Mac) build be added to the CI here? It should be relatively straightforward to adapt https://github.com/mit-plv/fiat-crypto/blob/master/.github/workflows/coq-opam-package.yml to test coqprime against whichever versions of Coq you want on Windows and MacOS

from coqprime.

don't lose too much time on this. It is ok to have only explicte output in a file.
I've removed the pipe in master

from coqprime.

Thanks!

I am currently running another CI run on Coq Platform in an attempt to get the autoconf file right. The handling of the math library "-lm" is strangely different on different OSes, even if all use a similar version of gcc.

If this runs through (I will ping you here), would you mind creating a new tag which includes the pipe change and my autoconf PR?

Btw.: I saw that you force pushed to master - I think you shouldn't and you should setup GitHub so that nobody can force push to master (there is an option in the settings). If the master branch is protected against force pushes nothing will ever get lost.

from coqprime.

Btw.: I saw that you force pushed to master - I think you shouldn't and you should setup GitHub so that nobody can force push to master (there is an option in the settings). If the master branch is protected against force pushes nothing will ever get lost.

My bad, didn't know there was a button to revert merge.
For the protection, it would make sense but I could not see anything. There is something but you need GitHub pro

from coqprime.

If this runs through (I will ping you here), would you mind creating a new tag which includes the pipe change and my autoconf PR?

no problem

from coqprime.

For the protection, it would make sense but I could not see anything.

It is fairly non obvious. Before there was a simple button under Settings/Branch. Now they have branch protection rules, but there is no rule against force push. The point is that having any branch protection rule disables force pushes and deletion, unless you enable it:

https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/defining-the-mergeability-of-pull-requests/about-protected-branches

So I would recommend to add a branch protection rule and just set the "include administrators" rule.

from coqprime.

Yes but I stopped when I saw

Protected branches are available in public repositories with GitHub Free and GitHub 
Free for organizations, and in public and private repositories with GitHub Pro, GitHub 
Team, GitHub Enterprise Cloud, and GitHub Enterprise Server. For more information, 
see "GitHub's products.

from coqprime.

Well it says

Protected branches are available in public repositories with GitHub Free

Your repo is a public repo. You couldn't do it for private repos.

from coqprime.

@thery : not sure if you have seen my comment in (#30). From my point of few your changes and this PR together would make a good tag for Coq Platform, but I can also keep my PR (and your changes as well) as opam level patches.

from coqprime.

sorry still fighting to understand how to disable force push by administrator.
I will merge and do the tag asap

from coqprime.

sorry still fighting to understand how to disable force push by administrator.

Go to https://github.com/thery/coqprime/settings/branch_protection_rules/new (or https://github.com/thery/coqprime/settings/branches and click "Add rule"), type "master" in the "Branch name pattern", and then click "create" (no need to check off any options). I think that's all that's required.

from coqprime.

@JasonGross

% git push -f
....
To github.com:thery/coqprime.git
 ! [remote rejected] master -> master (protected branch hook declined)
error: failed to push some refs to 'github.com:thery/coqprime.git

Perfect! Thanks

from coqprime.

no need to check off any options

I think you need to enable "Include administrators" (Enforce all configured restrictions above for administrators). Since you are likely administrator of your own project, the restrictions won't apply to you otherwise.

from coqprime.

@thery : unfortunately there is one more use of pipe in function certif.c - apparently for a similar purpose, so the Windows build still fails.

from coqprime.

@MSoegtropIMC oops, this looks more difficult. I will try to have a look tonight

from coqprime.

@MSoegtropIMC ok just committed something.
Now ./pocklington -size 20 should generate a .v with a 20-digits certified prime number even on Windows 🤞

from coqprime.

Thanks, I will test it!

Btw.: there would be a way to have a similar functionality in a portable way: redirect the data to a temporary file and read it from there.

There is also a function with a similar functionality as pipe on Windows, but parameters are different and the semantics are slightly different, but it should be OK for this case. So one could implement a pipe function on Windows.

from coqprime.

yes but there is no need to do all this in the first place, I was not the author of this bit of code, it is just trying to turn a gmp number into a string.

from coqprime.

Indeed one can reasonably expect the user to either provide an output file name or accept a fixed output name.

CI is running - bets are still open ;-)

I now linked the opam file to the specific commit on your master branch - if CI passes it would be nice if you move the tag to this commit.

Btw.: I plan to push opam packages "coq-coqprime.1.1.1" and "coq-coqprime-generator.1.1.1", but only after the gmp-emc package is accepted in the main opam repo - I didn't do a PR for this as yet, because I wanted to see Windows CI pass first.

from coqprime.

@thery : CI on Windows did run through with your latest change. Do you want to change the tag or should I go with the commit hash?

from coqprime.

@MSoegtropIMC Does the OCaml/opam GitHub action use the right Windows setup to catch issues like this?

from coqprime.

@JasonGross : I was talking about Coq Platform CI. For issues like this it doesn't matter much what Windows version you have. Coq Platform uses cygwin MinGW cross to build, so what the C compiler does and does not depends on the version of MinGW supplied by cygwin and hardly at all on the underlying Windows version.

from coqprime.

This works now, so I am closing this issue.

from coqprime.