Closed jpoiret closed 3 months ago
(and it has already caught something)
Which is good to know:
/home/runner/work/cubical/cubical/Cubical/Tactics/Reflection.agda:92,5-19
warning: -W[no]UserWarning
DEPRECATED: Use `withReduceDefs` instead of `dontReduceDefs`
when scope checking dontReduceDefs
Also closing, like #1051
Hi, this is a first try at adding a CI workflow using Agda master, without rebuilding it ourselves. It simply fetches the nightly release and uses that instead.
This seems to be working fine on my fork, see https://github.com/jpoiret/cubical/actions/runs/6158237986/job/16710596838 (and it has already caught something).
WDYT?