agda 2.6.1.2

[carlocab]

• Have you followed the guidelines for contributing?
• Have you checked that there aren't other open pull requests for the same formula update/change?
• Have you built your formula locally with brew install --build-from-source <formula>, where <formula> is the name of the formula you're submitting?
• Is your test running fine brew test <formula>, where <formula> is the name of the formula you're submitting?
• Does your build pass brew audit --strict <formula> (after doing brew install <formula>)?

---

This doesn't work for me yet locally, but I suspect there might be an issue with my system. Hoping CI will produce something better. Or, at least, more informative errors.

Cf. #65000, #55253, #65831

[mitchblank]

After this merges try seeing if cedille builds, since it depends_on agda

[carlocab]

Yes, I've had a look at cedille. It's not going to build; the formula uses bits of brew that have now been disabled. It needs a revamp...

[carlocab]

Error: agda: failed
An exception occurred within a child process:
  Timeout::Error: execution expired

Ugh. Does anyone know if there's a way to extend this timeout?

[SMillerDev]

@MikeMcQuaid any DSL for extending the test timeout?

[MikeMcQuaid]

@SMillerDev Nope, sorry. Probably just warrants the test being simplified.

[carlocab]

Tbf I suspect the test is excessive, and probably could be cut down too. Except I don't really know agda so I'm a bit hesitant to change too much about the test.

[carlocab]

@MikeMcQuaid Just to understand what I need to do about the test block: does the timeout apply to the entirety of the block, or just to the individual commands that it runs?

[gromgit]

Not an agda guru either, but I suspect cutting the test down to the stdlibiotest stuff (a.k.a. "Hello World") should be sufficient.

[carlocab]

I actually think it's the calls to cabal that are the useless part of the test block, but that might be from my having made calls to it about four dozen times now over the course of fixing this formula.

Update: Ok, guess they weren't so useless.

[carlocab]

Still working on this. FYI. Yep, should be good to merge if CI is green.

[chenrui333]

awesome work!! 💯

[BrewTestBot]

🤖 A scheduled task has triggered a merge.

[mietek]

It would have been nice to ping some of the previous contributors to this formula about the changes to this formula.

The removed test was useful, because it tested that the standard library has been properly installed, which is not trivial to get right, and in fact the formula has been installing a broken standard library in the past.

The removed caveats were useful, because people continue to be confused about the proper way to set up Agda:
https://twitter.com/lindsey/status/1479258217905491968

Why were the caveats removed? Was it just an omission or something else? We could replace the caveats by automatically modifying files in the user’s home directory upon installation, but this has been discouraged in the past.

Why was the compilation of the agda-mode elisp removed?

[carlocab]

The test was removed because it was failing due to the timeout. (See comments above.) The caveats were an omission. The agda-mode elisp compilation failed when I built this locally.

Pull requests to improve the formula are welcome.

Note that I don't use Agda. (See comments above.) I just picked this up because it had been impossible to build from source with the Agda formula for nearly a year. It would've been ideal for this to have been done by someone who actually uses Agda, but it didn't look like that was going to happen. Maybe you'd like to fix up the changes I made here.

[mietek]

I understand the removed test has started failing at some point due to changes in Homebrew. This seems to be a problem with these changes rather than with the test, which should only take seconds to run locally. How long did it take for you?

Regarding the caveats, what is the current policy on modifying files in the user’s home directory upon installation?

Specifically, can the formula do something like this:

• check that ~/.agda does not exist;
• create ~/agda;
• create ~/.agda/libraries containing #{HOMEBREW_PREFIX}/lib/agda/standard-library.agda-lib;
• create ~/.agda/defaults containing standard-library.

[carlocab]

This seems to be a problem with these changes rather than with the test

It seems to be a problem with virtualisation.

How long did it take for you?

I don't recall, but it didn't take long. It was only a problem in CI.

what is the current policy on modifying files in the user’s home directory upon installation?

This is not allowed by the sandbox. Attempting to modify files outside of HOMEBREW_PREFIX or HOMEBREW_TEMP will fail.

[mietek]

Thank you. I expect that the security policy also does not allow persisting an environment variable change to happen automatically upon installation?

Specifically, can the formula set AGDA_DIR to a path inside HOMEBREW_PREFIX so that Agda is always executed with this setting?

[carlocab]

You can create a wrapper script that sets AGDA_DIR before executing agda using write_env_script or env_script_all_files.