Normalizer: do not drop internal ascriptions #394
ci.yml
on: pull_request
build
/
build
21m 40s
Matrix: tests / ocaml-smoke
tests
/
check-stage3
7m 54s
tests
/
test-local
15m 41s
tests
/
binary-smoke
17s
tests
/
perf-canaries
24s
ciok
0s
Annotations
9 errors, 61 warnings, and 7 notices
|
tests / test-local
Diff failed for files /tests/error-messages/_output/Monoid.fst.json_output and /tests/error-messages/Monoid.fst.json_output.expected:
--- _output/Monoid.fst.json_output 2025-02-18 17:16:13.153743721 +0000
+++ Monoid.fst.json_output.expected 2025-02-18 17:13:28.510220362 +0000
@@ -454,12 +454,10 @@
Monoid.intro_monoid Prims.bool false xor
let lift_monoid_option m =
(let mult x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
- FStar.Pervasives.Native.Some (m.mult x0 y0)
- | _, _ -> FStar.Pervasives.Native.None)
- <:
- FStar.Pervasives.Native.option a)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
+ FStar.Pervasives.Native.Some (m.mult x0 y0)
+ | _, _ -> FStar.Pervasives.Native.None)
<:
FStar.Pervasives.Native.option a
in
|
|
tests / test-local
Diff failed for files /tests/error-messages/_output/Monoid.fst.output and /tests/error-messages/Monoid.fst.output.expected:
--- _output/Monoid.fst.output 2025-02-18 17:16:14.134741261 +0000
+++ Monoid.fst.output.expected 2025-02-18 17:13:28.510220362 +0000
@@ -454,12 +454,10 @@
Monoid.intro_monoid Prims.bool false xor
let lift_monoid_option m =
(let mult x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
- FStar.Pervasives.Native.Some (m.mult x0 y0)
- | _, _ -> FStar.Pervasives.Native.None)
- <:
- FStar.Pervasives.Native.option a)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x0, FStar.Pervasives.Native.Some y0 ->
+ FStar.Pervasives.Native.Some (m.mult x0 y0)
+ | _, _ -> FStar.Pervasives.Native.None)
<:
FStar.Pervasives.Native.option a
in
|
|
tests / test-local
Diff failed for files /tests/error-messages/_output/PatImps.fst.json_output and /tests/error-messages/PatImps.fst.json_output.expected:
--- _output/PatImps.fst.json_output 2025-02-18 17:16:24.334716498 +0000
+++ PatImps.fst.json_output.expected 2025-02-18 17:13:28.512220356 +0000
@@ -76,13 +76,9 @@
module PatImps
Declarations: [
let f1 x =
- (((match x with
- | [] -> 0
- | _ :: _ -> 1)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | [] -> 0
+ | _ :: _ -> 1)
<:
Prims.int
noeq
@@ -92,12 +88,8 @@
let f2 x =
- (((let PatImps.A #i = x in
- i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (let PatImps.A #i = x in
+ i)
<:
Prims.int
noeq
@@ -113,13 +105,9 @@
let f3 x =
- (((match x with
- | PatImps.B #i -> i
- | PatImps.C #i -> i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | PatImps.B #i -> i
+ | PatImps.C #i -> i)
<:
Prims.int
]
|
|
tests / test-local
Diff failed for files /tests/error-messages/_output/PatImps.fst.output and /tests/error-messages/PatImps.fst.output.expected:
--- _output/PatImps.fst.output 2025-02-18 17:16:24.608715842 +0000
+++ PatImps.fst.output.expected 2025-02-18 17:13:28.512220356 +0000
@@ -76,13 +76,9 @@
module PatImps
Declarations: [
let f1 x =
- (((match x with
- | [] -> 0
- | _ :: _ -> 1)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | [] -> 0
+ | _ :: _ -> 1)
<:
Prims.int
noeq
@@ -92,12 +88,8 @@
let f2 x =
- (((let PatImps.A #i = x in
- i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (let PatImps.A #i = x in
+ i)
<:
Prims.int
noeq
@@ -113,13 +105,9 @@
let f3 x =
- (((match x with
- | PatImps.B #i -> i
- | PatImps.C #i -> i)
- <:
- Prims.int)
- <:
- Prims.int)
+ (match x with
+ | PatImps.B #i -> i
+ | PatImps.C #i -> i)
<:
Prims.int
]
|
|
tests / test-local
Diff failed for files /tests/error-messages/_output/TuplePat.fst.json_output and /tests/error-messages/TuplePat.fst.json_output.expected:
--- _output/TuplePat.fst.json_output 2025-02-18 17:16:40.075674431 +0000
+++ TuplePat.fst.json_output.expected 2025-02-18 17:13:28.514220351 +0000
@@ -32,21 +32,17 @@
module TuplePat
Declarations: [
let mult x y =
- ((match x, y with
- | 0, 0 -> 0
- | x, y -> x * y)
- <:
- Prims.int)
+ (match x, y with
+ | 0, 0 -> 0
+ | x, y -> x * y)
<:
Prims.int
let mult2 x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
- | FStar.Pervasives.Native.None , _ -> 0
- | _, FStar.Pervasives.Native.None -> 0
- | _ -> 123)
- <:
- Prims.int)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
+ | FStar.Pervasives.Native.None , _ -> 0
+ | _, FStar.Pervasives.Native.None -> 0
+ | _ -> 123)
<:
Prims.int
]
|
|
tests / test-local
Diff failed for files /tests/error-messages/_output/TuplePat.fst.output and /tests/error-messages/TuplePat.fst.output.expected:
--- _output/TuplePat.fst.output 2025-02-18 17:16:40.298673817 +0000
+++ TuplePat.fst.output.expected 2025-02-18 17:13:28.514220351 +0000
@@ -32,21 +32,17 @@
module TuplePat
Declarations: [
let mult x y =
- ((match x, y with
- | 0, 0 -> 0
- | x, y -> x * y)
- <:
- Prims.int)
+ (match x, y with
+ | 0, 0 -> 0
+ | x, y -> x * y)
<:
Prims.int
let mult2 x y =
- ((match x, y with
- | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
- | FStar.Pervasives.Native.None , _ -> 0
- | _, FStar.Pervasives.Native.None -> 0
- | _ -> 123)
- <:
- Prims.int)
+ (match x, y with
+ | FStar.Pervasives.Native.Some x, FStar.Pervasives.Native.Some y -> x * y
+ | FStar.Pervasives.Native.None , _ -> 0
+ | _, FStar.Pervasives.Native.None -> 0
+ | _ -> 123)
<:
Prims.int
]
|
|
tests / test-local
Diff failed for files /tests/ide/emacs/_output/Fib.compute.ideout and /tests/ide/emacs/Fib.compute.ideout.expected:
--- _output/Fib.compute.ideout 2025-02-18 17:24:08.009937060 +0000
+++ Fib.compute.ideout.expected 2025-02-18 17:13:28.519220338 +0000
@@ -1,3 +1,3 @@
{"kind": "protocol-info", "rest": "[...]"}
{"kind": "response", "query-id": "1", "response": [], "status": "success"}
-{"kind": "response", "query-id": "2", "response": "(8 <: int) <: int", "status": "success"}
+{"kind": "response", "query-id": "2", "response": "8 <: int", "status": "success"}
|
|
tests / test-local
Process completed with exit code 2.
|
|
ciok
Process completed with exit code 1.
|
|
build / build:
FStar/stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/FStar/FStar/FStar/stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
build / build:
FStar/src/basic/FStarC.Plugins.fst#L85
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
build / build:
FStar/src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
build / build:
FStar/src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
build / build:
FStar/src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
build / build:
FStar/src/parser/FStarC.Parser.AST.fst#L772
(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.AST.fst(772,8-772,22):
- Global binding
'FStarC.Parser.AST.decl_to_string'
is recursive but not used in its body
|
|
build / build:
FStar/src/parser/FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14):
- Global binding
'FStarC.Parser.ToDocument.p_decl'
is recursive but not used in its body
|
|
build / build:
FStar/src/parser/FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13):
- Global binding
'FStarC.Parser.ToDocument.p_justSig'
is recursive but not used in its body
|
|
build / build:
FStar/src/parser/FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24):
- Global binding
'FStarC.Parser.ToDocument.p_disjunctivePattern'
is recursive but not used in its body
|
|
build / build:
FStar/src/parser/FStarC.Parser.ToDocument.fst#L1731
(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21):
- Global binding
'FStarC.Parser.ToDocument.p_maybeFocusArrow'
is recursive but not used in its body
|
|
tests / check-stage3:
FStar.Pervasives.fsti#L642
(345) * Warning 345 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(642,66-642,67):
- Inserted an unsafe type coercion in generated code from unit -> 'a -> 'a to
unit -> 'a -> 'b.
- This may be unsound in F#.
- See also /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(642,55-642,56)
|
|
tests / check-stage3:
FStar.FiniteSet.Base.fst#L137
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(137,4-137,10):
- Parameter 0 of subset is unused and must be eliminated for F#; add `[@@
remove_unused_type_parameters [0; ...]]` to the interface signature.
- This type definition is being dropped
|
|
tests / check-stage3:
FStar.FiniteSet.Base.fst#L144
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(144,4-144,9):
- Parameter 0 of equal is unused and must be eliminated for F#; add `[@@
remove_unused_type_parameters [0; ...]]` to the interface signature.
- This type definition is being dropped
|
|
tests / check-stage3:
FStar.FiniteSet.Base.fst#L151
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(151,4-151,12):
- Parameter 0 of disjoint is unused and must be eliminated for F#; add `[@@
remove_unused_type_parameters [0; ...]]` to the interface signature.
- This type definition is being dropped
|
|
tests / check-stage3:
dummy#L1
(345) * Warning 345:
- Inserted an unsafe type coercion in generated code from some_ref -> (obj,
obj) mreference to some_ref -> (unit, unit) mreference.
- This may be unsound in F#.
|
|
tests / check-stage3:
FStar.FiniteMap.Base.fst#L83
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(83,4-83,10):
- Parameter 0 of values is unused and must be eliminated for F#; add `[@@
remove_unused_type_parameters [0; ...]]` to the interface signature.
- This type definition is being dropped
|
|
tests / check-stage3:
FStar.FiniteMap.Base.fst#L90
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(90,4-90,9):
- Parameter 0 of items is unused and must be eliminated for F#; add `[@@
remove_unused_type_parameters [0; ...]]` to the interface signature.
- This type definition is being dropped
|
|
tests / check-stage3:
FStar.FiniteMap.Base.fst#L138
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(138,4-138,9):
- Parameter 0 of equal is unused and must be eliminated for F#; add `[@@
remove_unused_type_parameters [0; ...]]` to the interface signature.
- This type definition is being dropped
|
|
tests / check-stage3:
FStar.FiniteMap.Base.fst#L145
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(145,4-145,12):
- Parameter 0 of disjoint is unused and must be eliminated for F#; add `[@@
remove_unused_type_parameters [0; ...]]` to the interface signature.
- This type definition is being dropped
|
|
tests / check-stage3:
FStar.Pervasives.fsti#L55
(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.Monotonic.Witnessed.fsti(34,4-34,33):
- Expected parameter 'state of witnessed to be unused in its definition and eliminated
- See also /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(55,0-55,56)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04)
The Ubuntu-20.04 brownout takes place from 2025-02-01. For more details, see https://github.com/actions/runner-images/issues/11101
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.TSet.fst#L27
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(27,4-27,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst(293,8-293,25):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.GhostSet.fst#L23
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GhostSet.fst(23,4-23,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(86,12-86,15)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(126,12-126,15)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.MST.fst#L222
(330) * Warning 330 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(222,43-222,55):
- Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental
feature;it is subject to some redesign in the future. Please keep us
informed (on github etc.) about how you are using it
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.MST.fst#L247
(352) * Warning 352 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(247,42-247,60):
- Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE is not a
substitutive indexed effect combinator, it is better to make it one if
possible for better performance and ease of use
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-20.04):
FStar.GSet.fst#L23
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GSet.fst(23,4-23,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
FStar.TSet.fst#L27
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(27,4-27,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
FStar.GhostSet.fst#L23
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GhostSet.fst(23,4-23,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(86,12-86,15)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(126,12-126,15)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst(293,8-293,25):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59):
- Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level
letbinding are not encoded to the solver, you will only be able to reason
with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fst(75,14-75,28)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59):
- Definitions of inner let-rec get_acc and its enclosing top-level letbinding
are not encoded to the solver, you will only be able to reason with their
types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fst(124,10-124,17)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-latest):
FStar.MST.fst#L222
(330) * Warning 330 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(222,43-222,55):
- Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental
feature;it is subject to some redesign in the future. Please keep us
informed (on github etc.) about how you are using it
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.TSet.fst#L27
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(27,4-27,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst(293,8-293,25):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.GhostSet.fst#L23
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GhostSet.fst(23,4-23,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(86,12-86,15)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(126,12-126,15)
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.MST.fst#L222
(330) * Warning 330 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(222,43-222,55):
- Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental
feature;it is subject to some redesign in the future. Please keep us
informed (on github etc.) about how you are using it
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.MST.fst#L247
(352) * Warning 352 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(247,42-247,60):
- Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE is not a
substitutive indexed effect combinator, it is better to make it one if
possible for better performance and ease of use
|
|
tests / ocaml-smoke (fstar-src.tar.gz, ubuntu-22.04):
FStar.GSet.fst#L23
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GSet.fst(23,4-23,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
tests / test-local:
Hello.fst#L5
(272) * Warning 272 at Hello.fst(5,0-5,34):
- Top-level let-bindings must be total; this term may have effects
|
|
tests / test-local:
Part2.Free.fst#L132
(350) * Warning 350 at Part2.Free.fst(132,4-134,12):
- 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.
|
|
tests / test-local:
Part2.Free.fst#L133
(350) * Warning 350 at Part2.Free.fst(133,4-134,12):
- 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.
|
|
tests / test-local:
Part2.FreeFunExt.fst#L136
(350) * Warning 350 at Part2.FreeFunExt.fst(136,4-138,12):
- 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.
|
|
tests / test-local:
Part2.FreeFunExt.fst#L137
(350) * Warning 350 at Part2.FreeFunExt.fst(137,4-138,12):
- 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.
|
|
tests / test-local:
Part2.Par.fst#L40
(350) * Warning 350 at Part2.Par.fst(40,18-40,40):
- 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.
|
|
tests / test-local:
Part2.Par.fst#L48
(350) * Warning 350 at Part2.Par.fst(48,18-48,40):
- 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.
|
|
tests / test-local:
Part2.Par.fst#L105
(350) * Warning 350 at Part2.Par.fst(105,4-106,17):
- 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.
|
|
tests / test-local:
Part2.ST.fst#L26
(350) * Warning 350 at Part2.ST.fst(26,2-28,10):
- 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.
|
|
tests / test-local:
Part2.ST.fst#L27
(350) * Warning 350 at Part2.ST.fst(27,2-28,10):
- 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.
|
|
tests / perf-canaries:
DEFS_100#L1
time = 0.13
|
|
tests / perf-canaries:
DEFS_200#L1
time = 0.14
|
|
tests / perf-canaries:
DEFS_400#L1
time = 0.16
|
|
tests / perf-canaries:
DEFS_800#L1
time = 0.20
|
|
tests / perf-canaries:
DEFS_1600#L1
time = 0.28
|
|
tests / perf-canaries:
DEFS_3200#L1
time = 0.46
|
|
tests / perf-canaries:
DEFS_6400#L1
time = 0.84
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
fstar-repo
Expired
|
192 MB |
sha256:275e7e8064e0684d458bdb4567adb4e7f531472d517903b644f7708430468f15
|
|
|
fstar-src.tar.gz
Expired
|
4.24 MB |
sha256:c4e5c88a11065112a7bf38aca3fca05d8dd98e46c0ba9c599017e3cb1f40b1e3
|
|
|
fstar.tar.gz
Expired
|
129 MB |
sha256:0ea7c87b5b61451352d2b2be94df1adc9cb0029ae006397ac46f6eef1fcb3231
|
|