Skip to content

Commit

Permalink
Fix Coq tests (#349)
Browse files Browse the repository at this point in the history
* Run Coq tests when test files change

* Use Let in tests for older Coqs
  • Loading branch information
whonore authored Apr 13, 2024
1 parent e658dca commit 0694dbe
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 4 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/coq-tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ on:
- 'tox.ini'
- 'python/coqtop.py'
- 'python/xmlInterface.py'
- 'tests/test_coqtop.py'
- 'tests/coq/**'

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
Expand Down
10 changes: 7 additions & 3 deletions tests/coq/test_coqtop.py
Original file line number Diff line number Diff line change
Expand Up @@ -51,10 +51,12 @@ def test_rewind_start(coq: Coqtop) -> None:

def test_dispatch_rewind(coq: Coqtop) -> None:
"""Rewinding should cancel out in_script dispatches."""
succ, _, _, _ = coq.dispatch("#[local] Definition a := 0.")
assert coq.xml is not None
let = "#[local] Definition" if coq.xml.version >= (8, 19, 0) else "Let"
succ, _, _, _ = coq.dispatch(f"{let} a := 0.")
old_state = get_state(coq)

succ, _, _, _ = coq.dispatch("#[local] Definition x := 1.")
succ, _, _, _ = coq.dispatch(f"{let} x := 1.")
assert succ
coq.rewind(1)
assert old_state == get_state(coq)
Expand Down Expand Up @@ -117,7 +119,9 @@ def test_dispatch_correct(

def test_dispatch_unicode(coq: Coqtop) -> None:
"""Should be able to use unicode characters."""
succ, _, _, _ = coq.dispatch("#[local] Definition α := 0.")
assert coq.xml is not None
let = "#[local] Definition" if coq.xml.version >= (8, 19, 0) else "Let"
succ, _, _, _ = coq.dispatch(f"{let} α := 0.")
assert succ
succ, _, _, _ = coq.dispatch("Print α.")
assert succ
Expand Down

0 comments on commit 0694dbe

Please sign in to comment.