8000 Warn in test runner if -v not supported by lawcho · Pull Request #7490 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Warn in test runner if -v not supported #7490

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Sep 18, 2024
Merged

Warn in test runner if -v not supported #7490

merged 1 commit into from
Sep 18, 2024

Conversation

lawcho
Copy link
Contributor
@lawcho lawcho commented Sep 12, 2024

This PR makes the tester check that Agda was built with -fdebug,
before running tests that depend on Agda supporting -v for debug output.

The motivation is to make the test suite more developer-friendly:
I often forget to build Agda with -fdebug, and then am surprised when (seemingly arbitrary) tests fail on my machine (but not CI).

Related tickets:

andreasabel
andreasabel approved these changes Sep 12, 2024
View reviewed changes
Copy link
Member
@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@andreasabel andreasabel added infra: test suite Issues relating to the test suite (not in changelog) devx Developer Experience (IDE setup, linting, dev builds, etc.) (not in changelog) labels Sep 12, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Sep 12, 2024
@andreasabel
Copy link
Member

Could we add something to CI to ensure that this works / keeps working?
Maybe a run of cabal test where we select just the Fail part of the test tree so as to not cost too much time in CI.

@lawcho
Copy link
Contributor Author
lawcho commented Sep 13, 2024

Could we add something to CI to ensure that this works / keeps working? Maybe a run of cabal test where we select just the Fail part of the test tree so as to not cost too much time in CI.

I don't think this can be tested efficiently in CI:

I tested this locally with

$ AGDA_BIN=$(cabal list-bin agda -O0) cabal run agda-tests -O0 -- -p Issue1809
Build profile: -w ghc-9.4.8 -O0
In order, the following will be built (use -v for more details):
 - Agda-2.8.0 (test:agda-tests) (configuration changed)
Configuring Agda-2.8.0...
Preprocessing library for Agda-2.8.0..
Building library for Agda-2.8.0..
[  1 of 435] Compiling Agda.Interaction.ExitCode [Flags changed]
[  2 of 435] Compiling Agda.Termination.CutOff [Flags changed]
<snip>
[67 of 67] Compiling Main [Bugs.Tests changed]
[68 of 68] Linking /home/lawrence/oss/agda/tester-warn-unsupported-v/dist-newstyle/build/x86_64-linux/ghc-9.4.8/Agda-2.8.0/noopt/build/agda-tests/agda-tests [Objects changed]
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
@ Detected an Agda built without the '-fdebug' cabal flag,                  @
@ tests that rely on debugging output will be skipped.                      @
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

No JS node binary found, skipping JS tests.
all
  Succeed
    Issue1809: DISABLED (0.01s)

Ignored 1 disabled tests.
All 0 tests passed (0.01s)

$ AGDA_BIN=$(cabal list-bin agda -O0 -fdebug) cabal run agda-tests -O0 -fdebug -- -p Issue1809
Build profile: -w ghc-9.4.8 -O0
In order, the following will be built (use -v for more details):
 - Agda-2.8.0 (test:agda-tests) (configuration changed)
Configuring Agda-2.8.0...
Preprocessing library for Agda-2.8.0..
Building library for Agda-2.8.0..
[  1 of 435] Compiling Agda.Interaction.ExitCode [Flags changed]
[  2 of 435] Compiling Agda.Termination.CutOff [Flags changed]
<snip>
[67 of 67] Compiling Main [Bugs.Tests changed]
[68 of 68] Linking /home/lawrence/oss/agda/tester-warn-unsupported-v/dist-newstyle/build/x86_64-linux/ghc-9.4.8/Agda-2.8.0/noopt/build/agda-tests/agda-tests [Objects changed]
No JS node binary found, skipping JS tests.
all
  Succeed
    Issue1809: OK (0.14s)

All 1 tests passed (0.14s)

@andreasabel
Copy link
Member

It seems like cabal test is broken (on master), probably because it picks up the wrong Agda binary. (Same for this PR.)
I have not tried it in a long time.
In the environment set by cabal exec, the binary seems to be correct:

$ cabal exec -- which agda
/Users/abel/agda-erasure/dist-newstyle/build/x86_64-osx/ghc-9.10.1/Agda-2.8.0/build/agda/agda

So maybe our special logic for agdaBin sabotages this...
cabal run tests exhibits the same symptoms.

@lawcho
Copy link
Contributor Author
lawcho commented Sep 18, 2024

It seems like cabal test is broken (on master), probably because it picks up the wrong Agda binary

Indeed. I currently use:

AGDA_BIN=$(cabal list-bin agda -O0 -fdebug) cabal run agda-tests -O0 -fdebug

Where setting AGDA_BIN simultaneously tells the tester to...

  • Use a specific agda binary
  • Hide the "use the Makefile" banner
  • Enable latex tests
  • Enable stdlib compiler tests
  • Enable exec tests
  • Enable icu tests

I'd prefer these inputs to be decoupled, but that can be implemented in a separate PR.

@andreasabel
Copy link
Member
andreasabel 8000 commented Sep 18, 2024

Ok, I am merging this as-is now since I am not in the mood now to add a CI for this.
We can do this at some later stage.

Thanks for the contribution!

@andreasabel andreasabel self-assigned this Sep 18, 2024
@andreasabel andreasabel merged commit d567738 into agda:master Sep 18, 2024
24 checks passed
andreasabel
andreasabel reviewed Nov 9, 2024
View reviewed changes
test/Interactive/Tests.hs
[ disable "interaction/Debug"
, disable "interaction/Issue1353"
, disable "interaction/Positivity"
]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a mixup between Interactive (tests the decommissioned Agda repl) and interaction (tests the Agda interaction facilities).
The interaction tests are still run by a Makefile only, do not have a implementation as tasty-silver testsuite.
So I suppose this code is not doing anything here.
I'll proceed to remove it.
It would have to be ported to the Makefile, but as I understood, we are anyway not testing this PR in CI.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed in #7604.

andreasabel added a commit that referenced this pull request Nov 9, 2024
@andreasabel
Fixup #7490: remove stay test.Interactive.fdebugTestFilter
15194b3 
This code has no function, it was intended for the `interaction`
testsuite but this is not covered by our tasty-silver suite yet.
@andreasabel andreasabel mentioned this pull request Nov 9, 2024
Merged
AndrasKovacs pushed a commit that referenced this pull request Nov 19, 2024
@andreasabel @AndrasKovacs
Fixup #7490: remove stay test.Interactive.fdebugTestFilter
8fb863a 
This code has no function, it was intended for the `interaction`
testsuite but this is not covered by our tasty-silver suite yet.
fredins pushed a commit to fredins/agda that referenced this pull request Nov 24, 2024
@andreasabel @fredins
Fixup agda#7490: remove stay test.Interactive.fdebugTestFilter
7c647a0 
This code has no function, it was intended for the `interaction`
testsuite but this is not covered by our tasty-silver suite yet.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

Assignees

@andreasabel andreasabel

Labels
devx Developer Experience (IDE setup, linting, dev builds, etc.) (not in changelog) infra: test suite Issues relating to the test suite (not in changelog)
Projects
None yet
Milestone
2.8.0
Development

Successfully merging this pull request may close these issues.
2 participants
@lawcho @andreasabel
0