Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.json_output and /tests/error-messages/AQualMismatch.fst.json_output.expected: --- _output/AQualMismatch.fst.json_output 2025-01-17 06:22:35.889801682 +0000 +++ AQualMismatch.fst.json_output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,5 +1,5 @@ >> Got issues: [ -{"msg":["Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Error","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":8},"end_pos":{"line":6,"col":9}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":8},"end_pos":{"line":6,"col":9}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +{"msg":["Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Error","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} >>] -{"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":5},"end_pos":{"line":3,"col":6}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":5},"end_pos":{"line":3,"col":6}}},"number":240,"ctx":["While desugaring module AQualMismatch"]} -{"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":1},"end_pos":{"line":6,"col":13}}},"number":240,"ctx":[]} +{"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}}},"number":240,"ctx":["While desugaring module AQualMismatch"]} +{"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]}

Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.output and /tests/error-messages/AQualMismatch.fst.output.expected: --- _output/AQualMismatch.fst.output 2025-01-17 06:22:36.075802491 +0000 +++ AQualMismatch.fst.output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,14 +1,14 @@ >> Got issues: [ -* Error 91 at AQualMismatch.fst:6.8-6.9: +* Error 91 at AQualMismatch.fst(6,7-6,8): - Inconsistent implicit argument annotation on argument x - Got: '#' - Expected: '' >>] -* Warning 240 at AQualMismatch.fst:3.5-3.6: +* Warning 240 at AQualMismatch.fst(3,4-3,5): - AQualMismatch.f is declared but no definition was found - Add an 'assume' if this is intentional -* Warning 240 at AQualMismatch.fst:6.1-6.13: +* Warning 240 at AQualMismatch.fst(6,0-6,12): - Missing definitions in module AQualMismatch: f

Diff failed for files /tests/error-messages/_output/AnotType.fst.json_output and /tests/error-messages/AnotType.fst.json_output.expected: --- _output/AnotType.fst.json_output 2025-01-17 06:22:36.267803326 +0000 +++ AnotType.fst.json_output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,6 +1,6 @@ >> Got issues: [ -{"msg":["Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":6},"end_pos":{"line":19,"col":8}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":6},"end_pos":{"line":19,"col":8}}},"number":309,"ctx":["While typechecking the top-level declaration `type AnotType.tc`","While typechecking the top-level declaration `[@@expect_failure] type AnotType.tc`"]} +{"msg":["Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}}},"number":309,"ctx":["While typechecking the top-level declaration `type AnotType.tc`","While typechecking the top-level declaration `[@@expect_failure] type AnotType.tc`"]} >>] >> Got issues: [ -{"msg":["Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":15},"end_pos":{"line":27,"col":17}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":15},"end_pos":{"line":27,"col":17}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +{"msg":["Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>]

Diff failed for files /tests/error-messages/_output/AnotType.fst.output and /tests/error-messages/AnotType.fst.output.expected: --- _output/AnotType.fst.output 2025-01-17 06:22:36.515804405 +0000 +++ AnotType.fst.output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,11 +1,11 @@ >> Got issues: [ -* Error 309 at AnotType.fst:19.6-19.8: +* Error 309 at AnotType.fst(19,5-19,7): - Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers >>] >> Got issues: [ -* Error 189 at AnotType.fst:27.15-27.17: +* Error 189 at AnotType.fst(27,14-27,16): - Expected expression of type Type0 got expression tb of type Type >>]

Diff failed for files /tests/error-messages/_output/ArgsAndQuals.fst.json_output and /tests/error-messages/ArgsAndQuals.fst.json_output.expected: --- _output/ArgsAndQuals.fst.json_output 2025-01-17 06:22:36.741805387 +0000 +++ ArgsAndQuals.fst.json_output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,5 +1,5 @@ >> Got issues: [ -{"msg":["Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Error","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":17},"end_pos":{"line":25,"col":19}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":17},"end_pos":{"line":25,"col":19}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +{"msg":["Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Error","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} >>] -{"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":5},"end_pos":{"line":23,"col":10}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":5},"end_pos":{"line":23,"col":10}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]} -{"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":1},"end_pos":{"line":25,"col":30}}},"number":240,"ctx":[]} +{"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]} +{"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]}

Diff failed for files /tests/error-messages/_output/ArgsAndQuals.fst.output and /tests/error-messages/ArgsAndQuals.fst.output.expected: --- _output/ArgsAndQuals.fst.output 2025-01-17 06:22:36.916806148 +0000 +++ ArgsAndQuals.fst.output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,14 +1,14 @@ >> Got issues: [ -* Error 91 at ArgsAndQuals.fst:25.17-25.19: +* Error 91 at ArgsAndQuals.fst(25,16-25,18): - Inconsistent implicit argument annotation on argument uu___ - Got: '#' - Expected: '$' >>] -* Warning 240 at ArgsAndQuals.fst:23.5-23.10: +* Warning 240 at ArgsAndQuals.fst(23,4-23,9): - ArgsAndQuals.test1 is declared but no definition was found - Add an 'assume' if this is intentional -* Warning 240 at ArgsAndQuals.fst:25.1-25.30: +* Warning 240 at ArgsAndQuals.fst(25,0-25,29): - Missing definitions in module ArgsAndQuals: test1

Diff failed for files /tests/error-messages/_output/ArrowRanges.fst.json_output and /tests/error-messages/ArrowRanges.fst.json_output.expected: --- _output/ArrowRanges.fst.json_output 2025-01-17 06:22:37.182807305 +0000 +++ ArrowRanges.fst.json_output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,6 +1,6 @@ >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":73,"col":24},"end_pos":{"line":73,"col":31}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":4,"col":31},"end_pos":{"line":4,"col":40}}},"number":19,"ctx":["While typechecking the top-level declaration `let ppof`","While typechecking the top-level declaration `[@@expect_failure] let ppof`"]} +{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":4,"col":30},"end_pos":{"line":4,"col":39}}},"number":19,"ctx":["While typechecking the top-level declaration `let ppof`","While typechecking the top-level declaration `[@@expect_failure] let ppof`"]} >>] >> Got issues: [ -{"msg":["Failed to prove that the type\n'ArrowRanges.ppof'\nsupports decidable equality because of this argument.","Add either the 'noeq' or 'unopteq' qualifier","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ArrowRanges.fst","start_pos":{"line":7,"col":1},"end_pos":{"line":11,"col":2}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":8,"col":11},"end_pos":{"line":8,"col":29}}},"number":19,"ctx":["While typechecking the top-level declaration `type ArrowRanges.ppof`","While typechecking the top-level declaration `[@@expect_failure] type ArrowRanges.ppof`"]} +{"msg":["Failed to prove that the type\n'ArrowRanges.ppof'\nsupports decidable equality because of this argument.","Add either the 'noeq' or 'unopteq' qualifier","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ArrowRanges.fst","start_pos":{"line":7,"col":0},"end_pos":{"line":11,"col":1}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":8,"col":10},"end_pos":{"line":8,"col":28}}},"number":19,"ctx":["While typechecking the top-level declaration `type ArrowRanges.ppof`","While typechecking the top-level declaration `[@@expect_failure] type ArrowRanges.ppof`"]} >>]

Diff failed for files /tests/error-messages/_output/ArrowRanges.fst.output and /tests/error-messages/ArrowRanges.fst.output.expected: --- _output/ArrowRanges.fst.output 2025-01-17 06:22:37.452808479 +0000 +++ ArrowRanges.fst.output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,20 +1,20 @@ >> Got issues: [ -* Error 19 at ArrowRanges.fst:4.31-4.40: +* Error 19 at ArrowRanges.fst(4,30-4,39): - Subtyping check failed - Expected type Prims.eqtype got type Type0 - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst:73.24-73.31 + - See also Prims.fst(73,23-73,30) >>] >> Got issues: [ -* Error 19 at ArrowRanges.fst:8.11-8.29: +* Error 19 at ArrowRanges.fst(8,10-8,28): - Failed to prove that the type 'ArrowRanges.ppof' supports decidable equality because of this argument. - Add either the 'noeq' or 'unopteq' qualifier - The SMT solver could not prove the query. Use --query_stats for more details. - - See also ArrowRanges.fst:7.1-11.2 + - See also ArrowRanges.fst(7,0-11,1) >>]

Diff failed for files /tests/error-messages/_output/AssertNorm.fst.json_output and /tests/error-messages/AssertNorm.fst.json_output.expected: --- _output/AssertNorm.fst.json_output 2025-01-17 06:22:37.673809440 +0000 +++ AssertNorm.fst.json_output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,3 +1,3 @@ >> Got issues: [ -{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":15},"end_pos":{"line":7,"col":31}},"use":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":3},"end_pos":{"line":7,"col":14}}},"number":19,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":14},"end_pos":{"line":7,"col":30}},"use":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":2},"end_pos":{"line":7,"col":13}}},"number":19,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} >>]

Diff failed for files /tests/error-messages/_output/AssertNorm.fst.output and /tests/error-messages/AssertNorm.fst.output.expected: --- _output/AssertNorm.fst.output 2025-01-17 06:22:37.887810371 +0000 +++ AssertNorm.fst.output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,8 +1,8 @@ >> Got issues: [ -* Error 19 at AssertNorm.fst:7.3-7.14: +* Error 19 at AssertNorm.fst(7,2-7,13): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also AssertNorm.fst:7.15-7.31 + - See also AssertNorm.fst(7,14-7,30) >>]

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(272) * Warning 272 at Hello.fst:5.1-5.35: - Top-level let-bindings must be total; this term may have effects

(350) * Warning 350 at Part2.Free.fst:132.5-134.13: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Free.fst:133.5-134.13: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.FreeFunExt.fst:136.5-138.13: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.FreeFunExt.fst:137.5-138.13: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Par.fst:40.19-40.41: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Par.fst:48.19-48.41: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Par.fst:105.5-106.18: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.ST.fst:26.3-28.11: - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.