You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Progress 1/2: gerty-mainTests
File tests
Positive cases
well-formed syntax
checking tests/cases/positive/syntax/case.lam parses: OK
checking tests/cases/positive/syntax/functions.lam parses: OK
checking tests/cases/positive/syntax/implicits.lam parses: OK
checking tests/cases/positive/syntax/grading/funTyGradedBinder.lam parses: OK
checking tests/cases/positive/syntax/grading/grades.lam parses: OK
checking tests/cases/positive/syntax/grading/lamGradedBinder.lam parses: OK
checking tests/cases/positive/syntax/grading/tenGradedBinder.lam parses: OK
checking tests/cases/positive/syntax/grading/varInGrade.lam parses: OK
checking tests/cases/positive/syntax/grading/complexExprInGrade.lam parses: OK
checking tests/cases/positive/syntax/modality.lam parses: OK
checking tests/cases/positive/syntax/pairs.lam parses: OK
checking tests/cases/positive/syntax/records/canNameLastParam.lam parses: OK
checking tests/cases/positive/syntax/records/emptyBody.lam parses: OK
checking tests/cases/positive/syntax/records/justConstructor.lam parses: OK
checking tests/cases/positive/syntax/records/multipleFieldsSingleClause.lam parses: OK
checking tests/cases/positive/syntax/regression/funTyInPair.lam parses: OK
scope checking
checking tests/cases/positive/scope/grades.lam scope checks: OK
type-checking
checking tests/cases/positive/typing/builtins/modality.lam type checks: OK (0.05s)
checking tests/cases/positive/typing/builtins/nat.lam type checks: OK
checking tests/cases/positive/typing/builtins/pairs.lam type checks: FAIL (0.08s)
tests/Test.hs:60:
Expected file to type check, but got: During checking of top-level 'snd':
The following error occurred when type-checking (at ensure) 'y'
against a type 'a':
Expected type 'a' but got 'b (case x of [z] -> z)'
checking tests/cases/positive/typing/builtins/unit.lam type checks: OK (0.01s)
checking tests/cases/positive/typing/grading/implicits.lam type checks: OK (0.22s)
checking tests/cases/positive/typing/grading/infLub.lam type checks: FAIL
tests/Test.hs:60:
Expected file to type check, but got: During checking of top-level 't0':
The following error occurred when type-checking:
(.0 = .inf) is Falsifiable
checking tests/cases/positive/typing/grading/oneUseVarUsed.lam type checks: OK
checking tests/cases/positive/typing/grading/privacyLevels.lam type checks: OK (0.07s)
checking tests/cases/positive/typing/grading/securityLevels.lam type checks: OK (0.02s)
checking tests/cases/positive/typing/grading/zeroUseVarUnused.lam type checks: OK
checking tests/cases/positive/typing/inference/modality.lam type checks: OK (0.03s)
checking tests/cases/positive/typing/inference/pair.lam type checks: OK (0.04s)
checking tests/cases/positive/typing/inference/unit.lam type checks: OK (0.04s)
checking tests/cases/positive/typing/regression/snd.lam type checks: FAIL (0.03s)
tests/Test.hs:60:
Expected file to type check, but got: During checking of top-level 'snd':
The following error occurred when type-checking (at ensure) 'y'
against a type 'b (fst a b <x, y>)':
Expected type 'b (fst a b <x, y>)' but got 'b x'
checking tests/cases/positive/typing/simple/app.lam type checks: OK (0.07s)
checking tests/cases/positive/typing/simple/lam.lam type checks: OK (0.01s)
checking tests/cases/positive/typing/simple/lambdaTypeToType.lam type checks: OK (0.01s)
checking tests/cases/positive/typing/simple/pi.lam type checks: OK (0.03s)
checking tests/cases/positive/typing/simple/substitution.lam type checks: OK (0.04s)
checking tests/cases/positive/typing/simple/type0.lam type checks: OK
checking tests/cases/positive/typing/simple/var.lam type checks: OK (0.03s)
type-checking examples
checking examples/app.lam type checks: OK
checking examples/existential.lam type checks: FAIL
tests/Test.hs:60:
Expected file to type check, but got:
The following error occurred when parsing:
examples/existential.lam:6,18: Parse error
,<ERROR>
.1] Type 0) (b : [.1, .0] (x ...
checking examples/gradedApp.lam type checks: OK (0.02s)
checking examples/gradedComonad.lam type checks: OK (0.02s)
checking examples/gradedId.lam type checks: OK
checking examples/gradedPair.lam type checks: OK
checking examples/nuyts.lam type checks: FAIL (0.06s)
tests/Test.hs:60:
Expected file to type check, but got: During checking of top-level 'RIisoExampleLeft':
The following error occurred when type-checking:
(.1 = .inf) ∧ (.1 = .inf) is Falsifiable
checking examples/pairs.lam type checks: FAIL (0.16s)
tests/Test.hs:60:
Expected file to type check, but got: During checking of top-level 'snd':
The following error occurred when type-checking (at ensure) 'y'
against a type 'b (fst a b <x, y>)':
Expected type 'b (fst a b <x, y>)' but got 'b x'
checking examples/poly.lam type checks: OK (0.03s)
checking examples/syntax.lam type checks: OK (0.18s)
checking examples/talk.lam type checks: OK (0.07s)
checking examples/universal.lam type checks: OK (0.01s)
Negative cases
bad syntax
checking tests/cases/negative/syntax/namedLastParamInFunTy.lam doesn't parse: OK
checking tests/cases/negative/syntax/namedSortOfRecord.lam doesn't parse: OK
checking tests/cases/negative/syntax/qualifiedSig.lam doesn't parse: OK
ill-scoped
checking tests/cases/negative/scope/dupDefs1.lam doesn't scope check: OK
checking tests/cases/negative/scope/dupDefs2.lam doesn't scope check: OK
checking tests/cases/negative/scope/dupDefs3.lam doesn't scope check: OK
checking tests/cases/negative/scope/dupDefs4.lam doesn't scope check: OK
checking tests/cases/negative/scope/grading/unboundVarInFunGrade.lam doesn't scope check: OK
checking tests/cases/negative/scope/grading/unboundVarInLamGrade.lam doesn't scope check: OK
ill-typed
checking tests/cases/negative/typing/grading/mismatchedGradesForSucc.lam doesn't type check: OK
checking tests/cases/negative/typing/grading/implicits/noGradeIdTypeTooBig.lam doesn't type check: OK (0.02s)
checking tests/cases/negative/typing/grading/implicits/noGradeIdMult.lam doesn't type check: OK (0.02s)
checking tests/cases/negative/typing/grading/zeroUseVarUsed.lam doesn't type check: OK
checking tests/cases/negative/typing/grading/zeroUseVarUsedInType.lam doesn't type check: OK
checking tests/cases/negative/typing/modality/incorrectBoxingDifferingGrade.lam doesn't type check: OK
checking tests/cases/negative/typing/regression/missingParamDependentApplication.lam doesn't type check: OK
checking tests/cases/negative/typing/types/incorrectTypeForLambda.lam doesn't type check: OK
checking tests/cases/negative/typing/types/typeBadLevelSimple.lam doesn't type check: OK
6 out of 68 tests failed (1.49s)
The text was updated successfully, but these errors were encountered:
Thanks for this. A couple of these should be passing, but a couple are known to be failing and basically represent some deep work that needs doing. examples/existential.lam shouldn't be there though so I've moved that into a work-in-progress folder in b463537
Hello. Are these tests known to be failing?
The text was updated successfully, but these errors were encountered: