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

setup: Don't assume exe is built on --lib #7471

Merged
merged 1 commit into from
Sep 7, 2024
Merged

Conversation

alt-romes
Copy link
Contributor

@alt-romes alt-romes commented Sep 4, 2024

Cabal-3.12 introduces a breaking change which broke cabal install --lib Agda.

The reason is that previously, Cabal, for a Custom-build-type package, would /always/ build the executable, even if only the library was requested, and Agda's Setup.hs copyHook expects the executable to /always/ be available to compile the Agda standard lib. Now, Cabal won't build the executable if it is not required, so Agda's assumption will cause a crash when the executable isn't built.

The fix is simple: don't try to compile the Agda standard library if only the Agda Haskell library was requested, since only when installing the executable does the agda standard library need to be installed.

Co-authored-by: @sheaf

@andreasabel
Copy link
Member

The changes here are unfortunately not visible on our CI ---supposedly because cabal suppresses the output of Setup.hs with standard options (personally I use -j1 and get the output).
So I tried the PR locally.

Without it, Setup prints:

Generating Agda library interface files...
*** Warning!
*** Could not generate Agda library interface files.
*** Reason:
dist/build/agda/agda: readCreateProcess: posix_spawnp: does not exist (No such file or directory)
*** The attempted call to Agda was:
Agda_datadir=/private/var/folders/lg/qcd3v89j59l3m6520kr42bdm0000gn/T/cabal-install.-69097/dist-newstyle/tmp/src-69097/Agda-2.8.0/src/data dist/build/agda/agda --interaction --interaction-exit-on-error -Werror -v0 <<EOF
IOTCM "/private/var/folders/lg/qcd3v89j59l3m6520kr42bdm0000gn/T/cabal-install.-69097/dist-newstyle/tmp/src-69097/Agda-2.8.0/src/data/lib/prim/Agda/Builtin/Bool.agda" None Indirect (Cmd_load_no_metas "/private/var/folders/lg/qcd3v89j59l3m6520kr42bdm0000gn/T/cabal-install.-69097/dist-newstyle/tmp/src-69097/Agda-2.8.0/src/data/lib/prim/Agda/Builtin/Bool.agda")
...
EOF
*** Ignoring error, continuing installation...

With the PR, this part is no longer printed.

@alt-romes
Copy link
Contributor Author

The changes here are unfortunately not visible on our CI ---supposedly because cabal suppresses the output of Setup.hs with standard options (personally I use -j1 and get the output). So I tried the PR locally.

Without it, Setup prints:

Generating Agda library interface files...
*** Warning!
*** Could not generate Agda library interface files.
*** Reason:
dist/build/agda/agda: readCreateProcess: posix_spawnp: does not exist (No such file or directory)
*** The attempted call to Agda was:
Agda_datadir=/private/var/folders/lg/qcd3v89j59l3m6520kr42bdm0000gn/T/cabal-install.-69097/dist-newstyle/tmp/src-69097/Agda-2.8.0/src/data dist/build/agda/agda --interaction --interaction-exit-on-error -Werror -v0 <<EOF
IOTCM "/private/var/folders/lg/qcd3v89j59l3m6520kr42bdm0000gn/T/cabal-install.-69097/dist-newstyle/tmp/src-69097/Agda-2.8.0/src/data/lib/prim/Agda/Builtin/Bool.agda" None Indirect (Cmd_load_no_metas "/private/var/folders/lg/qcd3v89j59l3m6520kr42bdm0000gn/T/cabal-install.-69097/dist-newstyle/tmp/src-69097/Agda-2.8.0/src/data/lib/prim/Agda/Builtin/Bool.agda")
...
EOF
*** Ignoring error, continuing installation...

With the PR, this part is no longer printed.

Thanks for double checking. This is also what I observed.

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.

Excellent, thanks for lending your expertise!

Setup.hs Show resolved Hide resolved
@andreasabel andreasabel added the Setup.hs Concerning the Custom build type of Agda label Sep 4, 2024
@andreasabel andreasabel added this to the 2.7.0.1 milestone Sep 4, 2024
@andreasabel andreasabel added the ux: installation Getting Agda set up on your machine label Sep 4, 2024
Cabal-3.12 introduces a breaking change which broke `cabal install --lib Agda`.

The reason is that previously, Cabal, for a Custom-build-type package,
would /always/ build the executable, even if only the library was
requested, and Agda's Setup.hs copyHook expects the executable to
/always/ be available to compile the Agda standard lib. Now, Cabal won't
build the executable if it is not required, so Agda's assumption will
cause a crash when the executable isn't built.

The fix is simple: don't try to compile the Agda standard library if
only the Agda Haskell library was requested, since only when installing
the executable does the agda standard library need to be installed.

Co-authored-by: @sheaf
Co-authored-by: @andreasabel
@andreasabel andreasabel merged commit 4f82f9b into agda:master Sep 7, 2024
34 checks passed
@andreasabel
Copy link
Member

Cherry-picked for 2.7.0.1.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Setup.hs Concerning the Custom build type of Agda ux: installation Getting Agda set up on your machine
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants