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

Give more detail on creating customized versions #446

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

jfehrle
Copy link
Member

@jfehrle jfehrle commented Nov 16, 2024

Identical to #430, which was on branch "main" by mistake.

I'm happy to revise.

@jfehrle
Copy link
Member Author

jfehrle commented Nov 16, 2024

@MSoegtropIMC I appreciate the doc changes but they need to be corrected in a few ways. E.g. it is easy to get a tar ball for any commit or tag without releasing it. One should mention how this works rather than how to make a release in github. For the opam package the main problem is that most packages are in a different repo. Only the coq packages are in the repo you mentioned. As is this is very confusing. But as I said, just remove the doc changes and keep them in the separate PR.

As I recall, it took me at least 6-8 hours and to figure out how to do this stuff with your help over a couple days. It really shouldn't be that hard. Changing the instructions to do something else is another project. If you give me some guidance I'll try to revise it. Otherwise I fumble around with stuff that's not documented, kind of randomly trying one thing after another.

For the download, if I change the url to https://api.github.com/repos/jfehrle/coq/tarball/debug_pl_8_19 the build still seems to work even if I don't update the checksum. If I do a wget with that URL and checksum it, the checksum is different. So not sure what's happening.

For downloading in order to compute the checksum, should I recommend wget? I tried using curl but didn't find the right parameters.

@MSoegtropIMC
Copy link
Collaborator

@jfehrle : I can adjust your text and you can review it then. I just wanted it to be out of the Ltac2 debugger PR so that we can do this separately.

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