Skip to content

Commit af81da1

Browse files
committed
[ fix ] Expect show goals command to format result differently after Agda v2.7.0
1 parent 05021ed commit af81da1

File tree

2 files changed

+31
-15
lines changed

2 files changed

+31
-15
lines changed

lib/js/test/tests/Test__ShowGoals.bs.js

Lines changed: 14 additions & 9 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

test/tests/Test__ShowGoals.res

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,23 @@ let run = normalization => {
1717
let filteredResponses = responses->Array.filter(filteredResponse)
1818

1919
let filepath = Path.asset(filename)
20-
let expectedAllGoalsWarningsBody = `?0 : ℕ\n?1 : ℕ\n?2 : ℕ\n?3 : _11\nSort _10 [ at ${filepath}:11,19-31 ]\n_11 : _10 [ at ${filepath}:11,19-31 ]\n_14 : ℕ [ at ${filepath}:11,19-31 ]\n\n———— Errors ————————————————————————————————————————————————\nUnsolved constraints\n`
21-
22-
Assert.deepStrictEqual(
23-
filteredResponses,
24-
[DisplayInfo(AllGoalsWarnings("*All Goals, Errors*", expectedAllGoalsWarningsBody))],
25-
)
20+
21+
switch ctx.state.agdaVersion {
22+
| Some(version) =>
23+
let expectedAllGoalsWarningsBody = if Util.Version.gte(version, "2.7.0") {
24+
// Agda 2.7.0+ uses singular "Error" and no trailing newline
25+
`?0 : ℕ\n?1 : ℕ\n?2 : ℕ\n?3 : _11\nSort _10 [ at ${filepath}:11,19-31 ]\n_11 : _10 [ at ${filepath}:11,19-31 ]\n_14 : ℕ [ at ${filepath}:11,19-31 ]\n\n———— Error —————————————————————————————————————————————————\nUnsolved constraints`
26+
} else {
27+
// Agda < 2.7.0 uses plural "Errors" and has trailing newline
28+
`?0 : ℕ\n?1 : ℕ\n?2 : ℕ\n?3 : _11\nSort _10 [ at ${filepath}:11,19-31 ]\n_11 : _10 [ at ${filepath}:11,19-31 ]\n_14 : ℕ [ at ${filepath}:11,19-31 ]\n\n———— Errors ————————————————————————————————————————————————\nUnsolved constraints\n`
29+
}
30+
31+
Assert.deepStrictEqual(
32+
filteredResponses,
33+
[DisplayInfo(AllGoalsWarnings("*All Goals, Errors*", expectedAllGoalsWarningsBody))],
34+
)
35+
| None => Assert.fail("No Agda version found")
36+
}
2637
})
2738

2839
Async.it("should work", async () => {

0 commit comments

Comments
 (0)