Skip to content

Conversation

@shhyou
Copy link
Contributor

@shhyou shhyou commented Sep 22, 2025

The commits include two changes:

  1. Add doc/ prefix to the Everything.agda targets in GNUmakefile
  2. Make cabal a makefile variable, thus allowing the user to substitute a different command (or designate a specific binary).

I believe (1) is a leftover of #2184. This change stops two consecutive make listings calls from re-generating the documentation.

(2) allows the user to use custom commands, e.g. using stack:

$ ln -s stack-9.10.2.yaml stack.yaml
$ stack build
$ make listings CABAL_RUN_COMMAND='stack exec' AGDA_OPTIONS=

However, fix-whitespace, check-whitespace and test seem to be cabal-specific, so I only make the cabal path customizable.

CI: shhyou#1

Copy link
Contributor

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

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

I'm fine with the output of GenerateEverything going (back) to doc/, assuming everything else keeps working. But definitely @gallais and @MatthewDaggitt need to also look at this.

@shhyou
Copy link
Contributor Author

shhyou commented Sep 22, 2025

I believe GenerateEverything already puts Everything.agda in doc since #2184. This PR does not change its --out-dir.

@MatthewDaggitt
Copy link
Contributor

This seems a reasonable set of changes to me!

@shhyou
Copy link
Contributor Author

shhyou commented Oct 2, 2025

@gallais For the change from Everything.agda: to doc/Everything.agda: in Makefile, is that a correct change? Because I see that GenerateEverything already puts Everything.agda in doc/.

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.

Fix the CABAL env var

@shhyou
Copy link
Contributor Author

shhyou commented Oct 27, 2025

I think this is ready.

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.

A sorry, I seemed to have blocked this with my review.
Changes accepted!

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.

4 participants