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.

Sign up for GitHub

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

Jump to bottom

test_wholefile.v incompatible with 8.17 #698

Open
hendriktews opened this issue Apr 8, 2023 · 1 comment
Open

test_wholefile.v incompatible with 8.17 #698

hendriktews opened this issue Apr 8, 2023 · 1 comment
Assignees
@erikmd @CyrilAnac

Comments

@hendriktews
Copy link
Collaborator

The Hint Resolve command in ci/test_wholefile.v triggers a fatal warning in Coq 8.17. Test 060_coq-test-wholefile in ci/coq-tests.el fails therefore for 8.17.
hendriktews added a commit to hendriktews/PG that referenced this issue Apr 8, 2023
@hendriktews
ci/coq-tests: expect 060_coq-test-wholefile to fail for 8.17
1891f09 
See also ProofGeneral#698.
@hendriktews hendriktews mentioned this issue Apr 8, 2023
Merged
hendriktews added a commit that referenced this issue Apr 14, 2023
@hendriktews
ci/coq-tests: expect 060_coq-test-wholefile to fail for 8.17
dac9b5d 
See also #698.
@SnarkBoojum
Copy link

@hendriktews I've been trying to get in touch with you - especially about the Debian packaging for proofgeneral... could you contact me? I'm jpuydt and a Debian developer so you can guess a valid mail.

Thanks!

@hendriktews hendriktews mentioned this issue Dec 26, 2023
Open
hendriktews added a commit to hendriktews/PG that referenced this issue Dec 26, 2023
@hendriktews
ci/coq-tests: Disable tests test_wholefile.v tests
13d731a 
File ci/test_wholefile.v file is outdated, uses deprecated features,
is therefore prone to caues Coq errors and therefore causes the tests
that use this file to fail. See ProofGeneral#698 and commit
bd3615b.
hendriktews added a commit that referenced this issue Jan 2, 2024
@hendriktews
ci/coq-tests: Disable tests test_wholefile.v tests
a6ec628 
File ci/test_wholefile.v file is outdated, uses deprecated features,
is therefore prone to caues Coq errors and therefore causes the tests
that use this file to fail. See #698 and commit
bd3615b.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@erikmd erikmd

@CyrilAnac CyrilAnac

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@SnarkBoojum @erikmd @hendriktews @CyrilAnac