Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Travis test for size-solver compiles Agda but shouldn't #5037

Closed
andreasabel opened this issue Nov 6, 2020 · 0 comments
Closed

Travis test for size-solver compiles Agda but shouldn't #5037

andreasabel opened this issue Nov 6, 2020 · 0 comments
Labels
size-solver travis (not in changelog) type: bug Issues and pull requests about actual bugs

Comments

@andreasabel
Copy link
Member

The travis test named "Compiler tests, benchmark summary, and other test" takes now a felt eternity. It compiles Agda from scratch:

stack build size-solver "${BUILD_ARGS[@]}"
Agda-2.6.2: unregistering (local file changes: .stack-work/dist/x86_64-linux/Cabal-3.2.0.0/build/autogen/Paths_Agda.hs)
Agda       > configure (lib + exe)
Agda       > [1 of 2] Compiling Main             ( /home/travis/build/agda/agda/Setup.hs, /home/travis
/build/agda/agda/.stack-work/dist/x86_64-linux/Cabal-3.2.0.0/setup/Main.o )
Agda       > Linking /home/travis/build/agda/agda/.stack-work/dist/x86_64-linux/Cabal-3.2.0.0/setup/setup ...
Agda       > Configuring Agda-2.6.2...
Agda       > build (lib + exe)
Agda       > Preprocessing library for Agda-2.6.2..
Agda       > unused rules: 6
Agda       > Building library for Agda-2.6.2..
Agda       > [  1 of 392] Compiling Agda.Interaction.ExitCode
Agda       > [  2 of 392] Compiling Agda.Interaction.Highlighting.Dot.Base
Agda       > [  3 of 392] Compiling Agda.Termination.CutOff
Agda       > [  4 of 392] Compiling Agda FOO BAR BAZ

Something is going very wrong here...

A quick fix would be to turn off the CI for size-solver (which is of limited value anyway).
Or maybe someone has a clue why this is suddently happening.

@andreasabel andreasabel added type: bug Issues and pull requests about actual bugs travis (not in changelog) size-solver labels Nov 6, 2020
andreasabel added a commit that referenced this issue Nov 6, 2020
Takes too long, since it recompiles Agda from scratch.

```
stack build size-solver "${BUILD_ARGS[@]}"
Agda-2.6.2: unregistering (local file changes: .stack-work/dist/x86_64-linux/Cabal-3.2.0.0/build/autogen/Paths_Agda.hs)
Agda       > configure (lib + exe)
Agda       > [1 of 2] Compiling Main             ( /home/travis/build/agda/agda/Setup.hs, /home/travis
/build/agda/agda/.stack-work/dist/x86_64-linux/Cabal-3.2.0.0/setup/Main.o )
Agda       > Linking /home/travis/build/agda/agda/.stack-work/dist/x86_64-linux/Cabal-3.2.0.0/setup/setup ...
Agda       > Configuring Agda-2.6.2...
Agda       > build (lib + exe)
Agda       > Preprocessing library for Agda-2.6.2..
Agda       > unused rules: 6
Agda       > Building library for Agda-2.6.2..
Agda       > [  1 of 392] Compiling Agda.Interaction.ExitCode
Agda       > [  2 of 392] Compiling Agda.Interaction.Highlighting.Dot.Base
Agda       > [  3 of 392] Compiling Agda.Termination.CutOff
...
```
@andreasabel andreasabel changed the title Travis test for size-solver compiles Agda again Travis test for size-solver compiles Agda but shouldn't Nov 9, 2020
L-TChen added a commit to L-TChen/agda that referenced this issue Dec 22, 2020
L-TChen added a commit to L-TChen/agda that referenced this issue Dec 22, 2020
L-TChen added a commit to L-TChen/agda that referenced this issue Dec 22, 2020
L-TChen added a commit to L-TChen/agda that referenced this issue Dec 24, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
size-solver travis (not in changelog) type: bug Issues and pull requests about actual bugs
Projects
None yet
Development

No branches or pull requests

1 participant