CBORDetSize: account for the extra length field #64
Annotations
4 errors and 10 warnings
Everparse CI:
out.fail.batch/FAILAllBytesCompose.fst#L81
(66) * Error 66 at out.fail.batch/FAILAllBytesCompose.fst(81,6-87,85):
- Failed to resolve implicit argument ?57
of type Prims.bool
introduced for Instantiating implicit argument
|
Everparse CI:
out.fail.batch/FAILAllBytesCompose.fst#L83
(12) * Error 12 at out.fail.batch/FAILAllBytesCompose.fst(83,10-85,52):
- Expected type
EverParse3d.Interpreter.typ (*?u58*)
_
(*?u59*)
_
(*?u60*)
_
(*?u61*)
_
(*?u62*)
_
(*?u63*)
_
but
EverParse3d.Interpreter.T_with_comment "should_not_be_here"
(EverParse3d.Interpreter.T_denoted "should_not_be_here" dtyp__test1)
"Validating field should_not_be_here"
has type
EverParse3d.Interpreter.typ kind__test1
EverParse3d.Interpreter.Trivial
EverParse3d.Interpreter.Trivial
EverParse3d.Interpreter.Trivial
false
false
|
Everparse CI:
ulib/Prims.fst#L459
(19) * Error 19 at out.fail.batch/FAILAllBytesNotLast.fst(14,2-34,16):
- Could not prove goal #1
- The SMT solver could not prove the query. Use --query_stats for more
details.
- See also ulib/Prims.fst(459,77-459,89)
|
Everparse CI:
out.fail.batch/FAILAllBytesNotLast.fst#L43
(189) * Error 189 at out.fail.batch/FAILAllBytesNotLast.fst(43,53-43,67):
- Expected expression of type
EverParse3d.Kinds.parser_kind (*?u58*)
_
EverParse3d.Kinds.WeakKindStrongPrefix
got expression EverParse3d.Kinds.kind_all_bytes
of type
EverParse3d.Kinds.parser_kind false
EverParse3d.Kinds.WeakKindConsumesAll
|
Everparse CI:
dummy#L1
(274) * Warning 274:
- Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c'
in file "/__w/everparse/everparse/karamel/krmllib/C.fst".
- Rename "/__w/everparse/everparse/karamel/krmllib/C.fst" to avoid conflicts.
|
Everparse CI:
dummy#L1
(274) * Warning 274:
- Implicitly opening namespace 'cddl.pulse.ast.det.' shadows module 'c'
in file "/__w/everparse/everparse/karamel/krmllib/C.fst".
- Rename "/__w/everparse/everparse/karamel/krmllib/C.fst" to avoid conflicts.
|
Everparse CI:
dummy#L1
(361) * Warning 361 at Options.fst(594,0-597,15):
- Some #push-options have not been popped. Current depth is 1.
|
Everparse CI:
dummy#L1
(274) * Warning 274:
- Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c'
in file "/__w/everparse/everparse/karamel/krmllib/C.fst".
- Rename "/__w/everparse/everparse/karamel/krmllib/C.fst" to avoid conflicts.
|
Everparse CI:
dummy#L1
(242) * Warning 242 at Ast.fst(395,0-429,18):
- Definitions of inner let-rec seq and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: Ast.fst(397,12-397,15)
|
Everparse CI:
dummy#L1
(242) * Warning 242 at Ast.fst(1251,0-1256,14):
- Definitions of inner let-rec seq and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: Ast.fst(397,12-397,15)
|
Everparse CI:
dummy#L1
(361) * Warning 361 at src/lowparse/LowParse.BitFields.fst(1276,0-1276,29):
- Some #push-options have not been popped. Current depth is 1.
|
Everparse CI:
Target.fst#L958
(337) * Warning 337 at Target.fst(958,28-958,29):
- 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 '@'.
|
Everparse CI:
Target.fst#L1051
(337) * Warning 337 at Target.fst(1051,69-1051,70):
- 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 '@'.
|
Everparse CI:
Target.fst#L1395
(337) * Warning 337 at Target.fst(1395,54-1395,55):
- 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 '@'.
|
Set up job
1s
1s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Build RockyIsHere/actions-calculate-log-time@v0.2.4
3s
3s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Initialize containers
53s
53s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Cleanup
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "HOME=/home/user" | sudo tee -a $GITHUB_ENV
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run mtzguido/set-opam-env@master
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run opam install -y hex re ctypes sha sexplib
40s
40s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run actions/checkout@master
2s
2s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Try fetch built F*
16s
16s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Build F*
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Save built F*
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "FSTAR_HOME=$(pwd)/FStar" | sudo tee -a $GITHUB_ENV
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "FSTAR_EXE=$(pwd)/FStar/bin/fstar.exe" | sudo tee -a $GITHUB_ENV
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "$(pwd)/FStar/bin" | sudo tee -a $GITHUB_PATH
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run actions/checkout@master
1s
1s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Try fetch built karamel
2s
2s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Build karamel (if not cached)
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Save built karamel
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "KRML_HOME=$(pwd)/karamel" | sudo tee -a $GITHUB_ENV
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "KRML_EXE=$(pwd)/karamel/krml" | sudo tee -a $GITHUB_ENV
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "$(pwd)/karamel" | sudo tee -a $GITHUB_PATH
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run actions/checkout@master
1s
1s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Try fetch built pulse
6s
6s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Build pulse (if not cached)
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Save built pulse
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run echo "PULSE_HOME=$(pwd)/pulse"/out | sudo tee -a $GITHUB_ENV
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Run actions/checkout@master
1s
1s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Everparse CI
1h 35m 38s
1h 35m 38s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Incrementality test
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Calculate Time
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Post result to Zulip
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Post Run actions/checkout@master
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Post Run actions/checkout@master
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Post Run actions/checkout@master
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Post Run actions/checkout@master
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Stop containers
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Complete job
0s
0s
Error:
This step has been truncated due to its large size. Download the full logs from the menu
once the workflow run has completed.
Loading