Skip to content

Conversation

@MatthewDaggitt
Copy link
Collaborator

Cherry-picking @gallais's amazing work across from the v2.0-joss-submission branch. Resolved one merge-conflict in the ubuntu-ci workflow but hopefully this works 🤞

@gallais
Copy link
Member

gallais commented Nov 26, 2025

We'll need to bump some dependencies given we're using a newer GHC, a newer Agda, etc.
We'll also need to modify the run of the new test cases added since 2.0 to use the improved infra.
I might be able to take a look on Friday / this weekend.

@gallais gallais self-assigned this Dec 10, 2025
This is probably not going to build (missing bytestring / random
dependencies in the sample cabal file).
@gallais
Copy link
Member

gallais commented Dec 10, 2025

Alright, it now successfully builds on my machine. Let's see if CI agrees :)

* CI: remove JOSS build
* Test runner: print test name without buffering
* Script: fix issue leading to nested _build/_build/...
@gallais gallais changed the title [ fix ] add test runner (#2884) [ fix ] test runner to use cabal (#2884) Dec 10, 2025
@gallais gallais linked an issue Dec 10, 2025 that may be closed by this pull request
@dorchard
Copy link

Hm I'm having issues here, with Agda 2.6.4 and the head of the v2.0-joss-submission branch.

(base) dorchard@edud5aa agda-stdlib % AGDA_EXEC=agda GHC_EXEC=ghc-9.2.8 make testsuite 
/Library/Developer/CommandLineTools/usr/bin/make -C tests test GHC_EXEC="ghc-9.2.8" AGDA="agda -Werror +RTS -M4.0G -H3.5G -A128M -RTS" only=
cd admin/runtests && AGDA="agda -Werror +RTS -M4.0G -H3.5G -A128M -RTS" sh run

_build/MAlonzo/Code/System/Clock/Primitive.hs:34:25: error:
    Not in scope: data constructor ‘Boottime’
   |
34 | pattern C_bootTime_18 = Boottime
   |                         ^^^^^^^^

_build/MAlonzo/Code/System/Clock/Primitive.hs:35:32: error:
    Not in scope: data constructor ‘MonotonicCoarse’
   |
35 | pattern C_monotonicCoarse_20 = MonotonicCoarse
   |                                ^^^^^^^^^^^^^^^

_build/MAlonzo/Code/System/Clock/Primitive.hs:36:31: error:
    Not in scope: data constructor ‘RealtimeCoarse’
   |
36 | pattern C_realTimeCoarse_22 = RealtimeCoarse
   |                               ^^^^^^^^^^^^^^

_build/MAlonzo/Code/System/Clock/Primitive.hs:61:7: error:
    Not in scope: data constructor ‘Boottime’
   |
61 |       Boottime -> ()
   |       ^^^^^^^^

_build/MAlonzo/Code/System/Clock/Primitive.hs:62:7: error:
    Not in scope: data constructor ‘MonotonicCoarse’
   |
62 |       MonotonicCoarse -> ()
   |       ^^^^^^^^^^^^^^^

_build/MAlonzo/Code/System/Clock/Primitive.hs:63:7: error:
    Not in scope: data constructor ‘RealtimeCoarse’
   |
63 |       RealtimeCoarse -> ()
   |       ^^^^^^^^^^^^^^
usage: cp [-R [-H | -L | -P]] [-fi | -n] [-aclpSsvXx] source_file target_file
       cp [-R [-H | -L | -P]] [-fi | -n] [-aclpSsvXx] source_file ... target_directory
./runtests "agda -Werror +RTS -M4.0G -H3.5G -A128M -RTS" --interactive --timing --failure-file failures --only 
/bin/sh: ./runtests: No such file or directory
make[1]: *** [test] Error 127
make: *** [testsuite] Error 2
(base) dorchard@edud5aa agda-stdlib % agda --version
Agda version 2.6.4
(base) dorchard@edud5aa agda-stdlib % git log | head
commit 0c42bd93acba5bf198e70d5ba63e224f30e59bf9
Author: MatthewDaggitt <matthewdaggitt@gmail.com>
Date:   Thu Nov 27 15:42:12 2025 +0800

    Address @vidsinghal's comments

commit a431f7762062e85ca35bfec9baff77e14de97e3b
Author: G. Allais <guillaume.allais@ens-lyon.org>
Date:   Wed Nov 26 03:04:58 2025 +0000

(base) dorchard@edud5aa agda-stdlib % git pull
Already up to date.
(base) dorchard@edud5aa agda-stdlib % git branch
  master
* v2.0-joss-submission

@danielskatz
Copy link

associated with openjournals/joss-reviews#9241

@gallais
Copy link
Member

gallais commented Dec 15, 2025

I'm confused: you need to go back to clock-0.5.2 to get a library without e.g. Boottime but we require clock >= 0.8 && <0.9 in the build.

Did you purge the old build artefacts before trying again?

@dorchard
Copy link

Good point. I did this:

(base) dorchard@edud5aa agda-stdlib % make clean
find . -type f -name '*.agdai' -delete
rm -f Everything.agda EverythingSafe.agda
(base) dorchard@edud5aa agda-stdlib % cd tests
(base) dorchard@edud5aa tests % make clean
rm -rf runtests
rm -rf _config/_build
rm -rf _config/dist-newstyle
(base) dorchard@edud5aa tests % cd ..       
(base) dorchard@edud5aa agda-stdlib % AGDA_EXEC=agda GHC_EXEC=ghc-9.2.8 make testsuite

But still the same issue.

@gallais
Copy link
Member

gallais commented Dec 16, 2025

There should be some clues in tests/admin/runtests/logs/cabal-build

@dorchard
Copy link

dorchard commented Dec 16, 2025

The log file stops at:

[ 42 of 177] Compiling MAlonzo.Code.System.Clock.Primitive ( _build/MAlonzo/Code/System/Clock/Primitive.hs, /Users/dorchard/agda-stdlib/tests/admin/runtests/dist-newstyle/build/aarch64-osx/ghc-9.2.8/runtests-0.0/x/runtests/build/runtests/runtests-tmp/MAlonzo/Code/System/Clock/Primitive.o )

So the build is using clock version 0.8.4 but I notice that in the documentation https://hackage.haskell.org/package/clock-0.8.4/docs/System-Clock.html it says that Boottime (and others) are Linux specific (I am using mac OS) which would explain why I am getting this failure. So it seems like there might be some platform specific stuff here?

@gallais
Copy link
Member

gallais commented Dec 16, 2025

The source file on hackage does not contain ifdefs so I assumed it
meant there were default implementations for other architectures.

gallais added a commit to gallais/agda-stdlib that referenced this pull request Dec 16, 2025
@gallais
Copy link
Member

gallais commented Dec 16, 2025

I've opened #2900 aiming to restrict the clock types to the ones that
are supported across the board.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

System.Directory.Primitive - XdgDirectory problem

6 participants