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

Add opam file for HoTT library for Coq 8.16 #2291

Conversation

Alizter
Copy link
Contributor

@Alizter Alizter commented Sep 7, 2022

No description provided.

ps-id: 9e94288a-9911-45c3-92a4-9882d609c557
@Alizter Alizter force-pushed the ps/rr/add_opam_file_for_hott_library_for_coq_8_16 branch from 4019429 to a61d252 Compare September 7, 2022 16:39
@Alizter
Copy link
Contributor Author

Alizter commented Sep 7, 2022

I generated the sha512 by hand, but I am always a little frightened if I did it correctly. What is the way to check?

@palmskog
Copy link
Contributor

palmskog commented Sep 7, 2022

@Alizter what exactly does "by hand" mean? Is it different from running sha512sum <my-file>?

@palmskog palmskog merged commit 5407b32 into coq:master Sep 7, 2022
@palmskog
Copy link
Contributor

palmskog commented Sep 7, 2022

I think @MSoegtropIMC wants to know about this one.

@silene
Copy link
Contributor

silene commented Sep 7, 2022

I generated the sha512 by hand, but I am always a little frightened if I did it correctly. What is the way to check?

I usually run opam lint --check-upstream path/to/opam.

@Alizter
Copy link
Contributor Author

Alizter commented Sep 7, 2022

@Alizter what exactly does "by hand" mean? Is it different from running sha512sum <my-file>?

Yes that is what I mean. I was wondering if opam was supposed to do this for me or something.

I generated the sha512 by hand, but I am always a little frightened if I did it correctly. What is the way to check?

I usually run opam lint --check-upstream path/to/opam.

Thanks!

@Alizter Alizter deleted the ps/rr/add_opam_file_for_hott_library_for_coq_8_16 branch September 7, 2022 17:53
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.

3 participants