Comments (7)
I generally agree with your suggestions to move the more complex logic from the Makefile
to Agda.cabal
, but we should be careful that the interface does not get more complex. In particular, make up-to-date-stdlib
is really easy to remember in a way that some sequence of git submodule ...
and cabal run ...
isn't. The same goes for make workflows
. Having a canonical way to make these targets without having to pass any flags is a real added value.
from agda.
This is a great initiative. As a developer, I mostly use make type-check
(though increasingly replacing this with HLS), make quicker-install-bin
(for quick iterations), and make install-bin
(for running the test suite), plus for testing make test
, make quicktest
, make succeed
, make fail
, make interaction
, make std-lib-test
, make cubical-test
, etc (depending on which part of Agda I'm working on). I also occasionally need to pass in an argument for getting a binary with a custom suffix, and I always have to look up how exactly that works. Other that that there is mostly a lot of stuff that I don't understand and don't use.
from agda.
I have a default.nix
that also pulls in haskell-language-server
, which I prefer over make typecheck
(though on memory constrained systems I would probably use ghcid
instead). I switch between
$ cabal v2-build --ghc-options=-O0 --builddir=dist-newstyle -fdebug
$ cabal v2-build --ghc-options="-O2 -j" -foptimise-heavily --builddir=dist-optimise-heavily -fdebug -- agda
# ^^ these ghc-options are probably placebo but they're in my shell history
to iterate. Code is set up to use the agda
in dist-newstyle
so I can iterate on interactive testing and I have
BASE_DIR ?= /home/amelia/default/Projects/agda/dist-optimise-heavily/build/x86_64-linux/ghc-9.6.3/Agda-2.6.5/build/
AGDA_BIN := $(BASE_DIR)/agda/agda
AGDA_TESTS_BIN := $(BASE_DIR)/agda-tests/agda-tests
as my mk/config.mk
— so that make succeed
, make fail
, make interaction
use the optimised build. I also have a pair of shell scripts for making the next TestN.agda
in the root directory and for bumping the interface file version that are... extremely shell script, but I'm happy to share if anyone would find them useful 🙂
from agda.
I use cabal repl
instead of make type-check
. The make targets I use are install-bin-debug
, debug-install-quick
, and the various different test targets (succeed
, fail
, interaction
, std-lib-test
, etc).
I don't understand how you imagine non-phony targets would work. Binaries are put in weird system specific locations, and the rules for recompilation are non-trivial. Even if you manage it, it will complicate the Makefile a lot, and the only benefit is that the Makefile is no longer "unusual"?
from agda.
RE local builds & non-phony goals (@UlfNorell, @andreasabel)
the only benefit is that the Makefile is no longer "unusual"?
Another benefit is exploiting make
's timestamp-based early-cut-off.
I don't understand how you imagine non-phony targets would work.
- Write agda binaries to
build/
(rather than~/.local/bin/
) - Name agda binaries descriptively (rather than always
agda
), e.g.agda-quicker
agda-debug-quicker
agda-optimized
- Write non-phony
build/agda-*
targets to generate the binaries - Write phony
*-build
aliases for the non-phonybuild/agda-*
targets, e.g.build: build/agda-optimized quickbuild: build/agda-quicker debugbuild: build/agda-debug-quicker
- Rewrite
*-test
targets to depend on appropriate binaries, e.g.test: build/agda-optimized ... quicktest: build/agda-quicker ... std-lib-test: build/agda-optimized ...
- Rewrite phony
*-install
targets as thin wrappers, e.g.install: build/agda-optimized cp $< $(SYSTEM_INSTALL_DIR)/agda quickinstall: build/agda-quicker cp $< $(SYSTEM_INSTALL_DIR)/agda
- Use env vars (e.g.
DEBUG=1
) for build variants that shouldn't trigger a re-build on test
However, this assumes we keep the Makefile
at all.
Dropping the Makefile
and using cabal v2-build
directly also provides early-cut-off.
from agda.
You left out how to tell make
about the dependencies. For instance,
- All the Haskell sources
- The primitive libraries
- The emacs mode
- I did
cabal update
and want to rebuild dependencies - I switched ghc version
- Probably a bunch more that cabal keeps track of that's we'd have to encode manually
Another benefit is exploiting make's timestamp-based early-cut-off.
That only works if you can accurately encode the dependencies. At the moment cabal handles all that for us.
Rewrite phony *-install targets as thin wrappers
What about installing the primitive libraries and the emacs mode? Are you planning to write "thin" wrappers for those to?
However, this assumes we keep the Makefile at all.
- What's your vision for the test suites? What would I write to run only the stdlib tests (for instance)? What does that setup look like?
- What about other targets, like
make up-to-date-stdlib
ormake workflows
? - How do you work around the problem with
v2-build
followed byv2-install
rebuilding everything from scratch?
from agda.
You left out how to tell
make
about the dependencies.
build/agda-optimized: $(shell find src/full/)
would cover some of the dependencies.
At the moment cabal handles all that for us.
Yes. I'd prefer to drop the Makefile
entirely and use cabal v2-*
directly.
What's your vision for the test suites? What would I write to run only the stdlib tests (for instance)? What does that setup look like?
-
To run all the tests:
cabal test
-
To run std-lib tests:
cabal test std-lib
-
To run succeed tests:
cabal test succeed
-
To skip tests for
Opaque
:cabal test --test-option="--regex-excude=all/Succeed/Opaque"
-
Named sub-test-suites to be ported from
Makefile
toAgda.cabal
-
Docs for
cabal test
:~$ cabal test --help | head Run test-suites. Usage: cabal test [TARGETS] [FLAGS] Runs the specified test-suites, first ensuring they are up to date. Any test-suite in any package in the project can be specified. A package can be specified in which case all the test-suites in the package are run. The default is to run all the test-suites in the package in the current directory.
make up-to-date-stdlib
First, run git submodule update --init std-lib
(my IDE's git
integration reminds me to do this anyway).
Then manually call make -C std-lib setup
Or (cd std-lib; cabal run GenerateEverything -- --out-dir doc)
,
since that is what the stdlib's Makefile ends up running.
Or don't run GenerateEverything
at all.
It appears to only generate documentation and is not mentioned in the stdlib install instructions,
so the test suite should work without it.
make workflows
?
make -C .github/workflows
How do you work around the problem with
v2-build
followed byv2-install
rebuilding everything from scratch?
Don't call v2-install
. Instead cabal exec install
.
Where the install
target is backed by glue currently in Setup.hs
.
from agda.
Related Issues (20)
- Internal error in Mimer with module parameter and matching
- Instance resolution failure in Agda 2.6.4 HOT 6
- Mimer drops part of the solution with module parameter
- Citation.cff HOT 1
- Delete the GitHub Wiki HOT 3
- Migrate the Chalmers Wiki HOT 4
- Prune `Setup.hs` HOT 5
- Reorganize `HACKING.md`
- Merge `.authorspellings` and `.mailmap` HOT 1
- Mimer internal error when querying `recRecursive` HOT 1
- Interactive highlighting remnants with lambda-where
- Pattern synonyms with named arguments can be defined but not used HOT 3
- Automatically create names for syntax
- Mangled trX/Con clause for indexed type with green slime HOT 1
- Why do we `reduce` and `instantiateFull` constraints? HOT 2
- Use of Non-terminating Function in Data Declaration Makes Typechecker Loop HOT 4
- Misprinted domain-free parameters with cohesion attribute HOT 1
- Regression in 2.6.4.2 concerning `with` HOT 6
- Regression in 2.6.4 in `rewrite` with instances
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda.