Skip to content

Commit

Permalink
Make tests for #641 less brittle (#7075)
Browse files Browse the repository at this point in the history
make tests for #641 less brittle
  • Loading branch information
UlfNorell committed Jan 30, 2024
1 parent eef3683 commit 1179610
Show file tree
Hide file tree
Showing 4 changed files with 2 additions and 106 deletions.
75 changes: 0 additions & 75 deletions test/Fail/Issue641-all-interfaces.err
Original file line number Diff line number Diff line change
@@ -1,80 +1,5 @@
Importing the primitive modules.
Getting interface for Agda.Primitive
Check for cycle
Agda.Primitive is not up-to-date because the interface has not been decoded and we're ignoring all interface files.
Checking Agda.Primitive (agda-default-include-path/Agda/Primitive.agda).
Creating interface for Agda.Primitive.
visited:
Starting scope checking.
Finished scope checking.
Starting highlighting from scope.
Finished highlighting from scope.
Starting type checking.
Finished type checking.
Starting highlighting from type info.
Finished highlighting from type info.
Starting serialization.
Building interface...
instantiating all meta variables
interface complete
Finished serialization.
Considering writing to interface file.
Actually calling writeInterface.
Writing interface file agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive.agdai.
Wrote interface file.
Finished writing to interface file.
Accumulated statistics.
Finished Agda.Primitive.
imports: []
New module. Let's check it out.
Merging interface
Now we've looked at Agda.Primitive
Getting interface for Agda.Primitive.Cubical
Check for cycle
Agda.Primitive.Cubical is not up-to-date because the interface has not been decoded and we're ignoring all interface files.
Checking Agda.Primitive.Cubical (agda-default-include-path/Agda/Primitive/Cubical.agda).
Creating interface for Agda.Primitive.Cubical.
visited: Agda.Primitive
Starting scope checking.
Scope checking Agda.Primitive
visited: Agda.Primitive
Already visited Agda.Primitive
Finished scope checking.
Starting highlighting from scope.
Finished highlighting from scope.
Starting type checking.
Finished type checking.
Starting highlighting from type info.
Finished highlighting from type info.
Starting serialization.
Building interface...
Already visited Agda.Primitive
instantiating all meta variables
interface complete
Finished serialization.
Considering writing to interface file.
Actually calling writeInterface.
Writing interface file agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive/Cubical.agdai.
Wrote interface file.
Finished writing to interface file.
Accumulated statistics.
Finished Agda.Primitive.Cubical.
imports: [(Agda.Primitive, 450520314077838934)]
Already visited Agda.Primitive
New module. Let's check it out.
Merging interface
Now we've looked at Agda.Primitive.Cubical
Done importing the primitive modules.
Getting interface for Issue641-all-interfaces
Check for cycle
Issue641-all-interfaces is not up-to-date because the interface has not been decoded and we're ignoring all interface files.
Checking Issue641-all-interfaces (Issue641-all-interfaces.agda).
Creating interface for Issue641-all-interfaces.
visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
visited: Agda.Primitive, Agda.Primitive.Cubical
Already visited Agda.Primitive
Issue641-all-interfaces.agda:9,6-18
No module NoSuchModule in scope
when scope checking the declaration
Expand Down
2 changes: 1 addition & 1 deletion test/Fail/Issue641-all-interfaces.flags
Original file line number Diff line number Diff line change
@@ -1 +1 @@
-v import:10 --ignore-all-interfaces
-v import.main:10 --ignore-all-interfaces
29 changes: 0 additions & 29 deletions test/Fail/Issue641.err
Original file line number Diff line number Diff line change
@@ -1,34 +1,5 @@
Importing the primitive modules.
Getting interface for Agda.Primitive
Check for cycle
Agda.Primitive is up-to-date.
no stored version, reading agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive.agdai
Loading Agda.Primitive (agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive.agdai).
imports: []
New module. Let's check it out.
Merging interface
Now we've looked at Agda.Primitive
Getting interface for Agda.Primitive.Cubical
Check for cycle
Agda.Primitive.Cubical is up-to-date.
no stored version, reading agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive/Cubical.agdai
Loading Agda.Primitive.Cubical (agda-default-include-path/_build/2.6.4.1/agda/Agda/Primitive/Cubical.agdai).
imports: [(Agda.Primitive, 450520314077838934)]
Already visited Agda.Primitive
New module. Let's check it out.
Merging interface
Now we've looked at Agda.Primitive.Cubical
Done importing the primitive modules.
Getting interface for Issue641
Check for cycle
Issue641 is not up-to-date because the interface has not been decoded and we're ignoring non-builtin interface files.
Checking Issue641 (Issue641.agda).
Creating interface for Issue641.
visited: Agda.Primitive, Agda.Primitive.Cubical
Starting scope checking.
Scope checking Agda.Primitive
visited: Agda.Primitive, Agda.Primitive.Cubical
Already visited Agda.Primitive
Issue641.agda:9,6-18
No module NoSuchModule in scope
when scope checking the declaration
Expand Down
2 changes: 1 addition & 1 deletion test/Fail/Issue641.flags
Original file line number Diff line number Diff line change
@@ -1 +1 @@
-v import:10 --ignore-interfaces
-v import.main:10 --ignore-interfaces

0 comments on commit 1179610

Please sign in to comment.