Check world (test F* + all subprojects) #72
Annotations
10 errors and 11 warnings
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.Sugar.fst#L25
(72) * Error 72 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(25,23-25,28):
- Identifier not found: [FStarC.Range.range]
- Could not resolve module name FStarC.Range
|
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.Err.fst#L19
(128) * Error 128 at src/syntax_extension/PulseSyntaxExtension.Err.fst(19,18-19,23):
- Module FStarC.Range cannot be found
|
Build (after setting up cargo env):
src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti#L20
(72) * Error 72 at src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti(20,25-20,30):
- Identifier not found: [FStarC.Range.range]
- Could not resolve module name FStarC.Range
|
Build (after setting up cargo env):
src/extraction/ExtractPulseOCaml.fst#L10
(134) * Error 134 at src/extraction/ExtractPulseOCaml.fst(10,12-10,18):
- Namespace FStarC.Effect cannot be found
|
Build (after setting up cargo env):
src/extraction/ExtractPulseC.fst#L5
(134) * Error 134 at src/extraction/ExtractPulseC.fst(5,12-5,18):
- Namespace FStarC.Effect cannot be found
|
Build (after setting up cargo env):
src/extraction/ExtractPulse.fst#L5
(134) * Error 134 at src/extraction/ExtractPulse.fst(5,12-5,18):
- Namespace FStarC.Effect cannot be found
|
Build (after setting up cargo env):
dummy#L1
(189) * Error 189 at src/checker/Pulse.Common.fst(63,0-68,16):
- Expected expression of type
f: (_: (*?u95*) _ -> FStar.Pervasives.Native.option (*?u90*) _) -> Type
got expression fun _ -> (*?u95*) _
of type
f: (_: (*?u95*) _ -> FStar.Pervasives.Native.option (*?u90*) _)
-> Prims.GTot Type
|
Build (after setting up cargo env):
lib/core/Pulse.Lib.NonInformative.fst#L32
(54) * Error 54 at lib/core/Pulse.Lib.NonInformative.fst(32,21-33,62):
- (*?u42*) _ is not equal to the expected type y: a{y == FStar.Ghost.elift1 (fun _ -> _._1) p} & (*?u12*) _
|
Build (after setting up cargo env):
lib/core/PulseCore.PartialNondeterministicHoareStateMonad.fsti#L20
(54) * Error 54 at lib/core/PulseCore.PartialNondeterministicHoareStateMonad.fsti(20,52-20,53):
- _: Prims.unit -> Prims.nat is not a subtype of the expected type _: Prims.unit -> FStar.Pervasives.Dv (k: Prims.nat{k == n})
- See also lib/core/PulseCore.PartialNondeterministicHoareStateMonad.fsti(20,14-20,15)
|
Build (after setting up cargo env):
lib/core/PulseCore.HeapExtension.fsti#L291
(66) * Error 66 at lib/core/PulseCore.HeapExtension.fsti(291,25-291,32):
- Failed to resolve implicit argument ?24
of type Type
introduced for Instantiating implicit argument
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
Build (after setting up cargo env):
src/extraction/ExtractPulse.fst#L5
(285) * Warning 285 at src/extraction/ExtractPulse.fst(5,12-5,18):
- No modules in namespace FStarC.Effect and no file with that name either
|
Build (after setting up cargo env):
src/extraction/ExtractPulse.fst#L6
(285) * Warning 285 at src/extraction/ExtractPulse.fst(6,12-6,16):
- No modules in namespace FStarC.List and no file with that name either
|
Build (after setting up cargo env):
src/extraction/ExtractPulse.fst#L7
(285) * Warning 285 at src/extraction/ExtractPulse.fst(7,12-7,16):
- No modules in namespace FStarC.Util and no file with that name either
|
Build (after setting up cargo env):
src/extraction/ExtractPulse.fst#L14
(285) * Warning 285 at src/extraction/ExtractPulse.fst(14,19-14,23):
- module not found in search path: fstarc.util
|
Build (after setting up cargo env):
src/extraction/ExtractPulseC.fst#L5
(285) * Warning 285 at src/extraction/ExtractPulseC.fst(5,12-5,18):
- No modules in namespace FStarC.Effect and no file with that name either
|
Build (after setting up cargo env):
src/extraction/ExtractPulseC.fst#L6
(285) * Warning 285 at src/extraction/ExtractPulseC.fst(6,12-6,16):
- No modules in namespace FStarC.List and no file with that name either
|
Build (after setting up cargo env):
src/extraction/ExtractPulseC.fst#L7
(285) * Warning 285 at src/extraction/ExtractPulseC.fst(7,12-7,16):
- No modules in namespace FStarC.Util and no file with that name either
|
Build (after setting up cargo env):
src/extraction/ExtractPulseC.fst#L15
(285) * Warning 285 at src/extraction/ExtractPulseC.fst(15,19-15,23):
- module not found in search path: fstarc.util
|
Build (after setting up cargo env):
src/extraction/ExtractPulseOCaml.fst#L10
(285) * Warning 285 at src/extraction/ExtractPulseOCaml.fst(10,12-10,18):
- No modules in namespace FStarC.Effect and no file with that name either
|
Build (after setting up cargo env):
src/extraction/ExtractPulseOCaml.fst#L11
(285) * Warning 285 at src/extraction/ExtractPulseOCaml.fst(11,12-11,16):
- No modules in namespace FStarC.List and no file with that name either
|
Loading