Disable eta-expansion in MLish #116
ci.yml
on: push
build
/
build
20m 7s
nix
/
fstar-nix
18m 56s
stale-hints
/
check_stale_hints
10s
Matrix: tests / binary-smoke
Matrix: tests / ocaml-smoke
tests
/
check-stage3
6m 42s
tests
/
test-local
14m 1s
tests
/
perf-canaries
16s
ciok
0s
Annotations
3 errors, 6 warnings, and 7 notices
tests / test-local
Diff failed for files /tests/error-messages/_output/NegativeTests.Neg.fst.json_output and /tests/error-messages/NegativeTests.Neg.fst.json_output.expected:
--- _output/NegativeTests.Neg.fst.json_output 2025-01-10 23:16:35.858124837 +0000
+++ NegativeTests.Neg.fst.json_output.expected 2025-01-10 23:13:39.195604026 +0000
@@ -20,7 +20,7 @@
{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.Native.option 'a {Some? _}\ngot type FStar.Pervasives.Native.option 'a","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.Native.fst","start_pos":{"line":33,"col":4},"end_pos":{"line":33,"col":8}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":46,"col":30},"end_pos":{"line":46,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_projector`","While typechecking the top-level declaration `[@@expect_failure] let bad_projector`"]}
>>]
>> Got issues: [
-{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":523,"col":4},"end_pos":{"line":523,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]}
+{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":520,"col":4},"end_pos":{"line":520,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]}
>>]
>> Got issues: [
{"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","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":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]}
|
tests / test-local
Diff failed for files /tests/error-messages/_output/NegativeTests.Neg.fst.output and /tests/error-messages/NegativeTests.Neg.fst.output.expected:
--- _output/NegativeTests.Neg.fst.output 2025-01-10 23:16:36.046123268 +0000
+++ NegativeTests.Neg.fst.output.expected 2025-01-10 23:13:39.195604026 +0000
@@ -63,7 +63,7 @@
got type FStar.Pervasives.result Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also FStar.Pervasives.fsti(523,4-523,5)
+ - See also FStar.Pervasives.fsti(520,4-520,5)
>>]
>> Got issues: [
|
tests / test-local
Process completed with exit code 2.
|
stale-hints / check_stale_hints
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
nix / fstar-nix
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
build / build
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
tests / check-stage3
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
tests / test-local
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
tests / perf-canaries:
DEFS_100#L1
time = 0.15
|
tests / perf-canaries:
DEFS_200#L1
time = 0.16
|
tests / perf-canaries:
DEFS_400#L1
time = 0.18
|
tests / perf-canaries:
DEFS_800#L1
time = 0.23
|
tests / perf-canaries:
DEFS_1600#L1
time = 0.30
|
tests / perf-canaries:
DEFS_3200#L1
time = 0.50
|
tests / perf-canaries:
DEFS_6400#L1
time = 0.84
|
Artifacts
Produced during runtime
Name | Size | |
---|---|---|
fstar-repo
|
311 MB |
|
fstar-src.tar.gz
|
4.98 MB |
|
fstar.tar.gz
|
137 MB |
|