Nightly #99
nikswamyAnnotations
5 errors and 1 warning
|
verify
Process completed with exit code 2.
|
|
verify:
CLRS.Ch02.InsertionSort.Rubric.fst#L289
(19) * Error 19 at CLRS.Ch02.InsertionSort.Rubric.fst(289,10-289,35):
- Failed to prove pure property: ‘SZ.v __vi4748 > 0’
- Assertion failed
|
|
verify:
CLRS.Ch02.MergeSort.Impl.fst#L259
(19) * Error 19 at CLRS.Ch02.MergeSort.Impl.fst(259,8-259,80):
- Failed to prove pure property:
‘Seq.index _s84 (SZ.v __vk5051) == Seq.index ghost_merged (SZ.v __vk5051)’
- Assertion failed
- See also CLRS.Ch02.MergeSort.Impl.fst(259,8-259,74)
|
|
verify:
CLRS.Ch06.Heap.Rubric.fst#L542
(228) * Error 228 at CLRS.Ch06.Heap.Rubric.fst(542,0-667,1):
- Tactic failed
- recursive functions require a 'decreases' clause to prove termination;
- use 'divergent fn' for a possibly non-terminating recursive function.
|
|
verify:
CLRS.Ch07.Quicksort.Rubric.fst#L356
(228) * Error 228 at CLRS.Ch07.Quicksort.Rubric.fst(356,0-417,1):
- Tactic failed
- recursive functions require a 'decreases' clause to prove termination;
- use 'divergent fn' for a possibly non-terminating recursive function.
|
|
verify
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
|