Andreas Abel
Andreas Abel
And BOOM! I did finally manage to show the current size-preservation analysis inconsistent: ```agda {-# OPTIONS --type-based-termination #-} data ⊥ : Set where record _×_ (A B : Set) :...
The use of `with` is (expectedly) also affected, you can swap `f` for this implementation: ```agda f : U → U × ⊥ f u with u ... | u'...
So we could have a flag `Werror` that turns the warnings into errors. That flag would be on for developers (set in `cabal.project` but by default off in `Agda.cabal` so...
I does not matter which words I use if the addressee never reacts.
``` X-Mozilla-Status: 0001 X-Mozilla-Status2: 00000000 Received: from GVZP280MB1863.SWEP280.PROD.OUTLOOK.COM (2603:10a6:150:237::6) by GVYP280MB0365.SWEP280.PROD.OUTLOOK.COM with HTTPS; Tue, 7 Jan 2025 07:57:49 +0000 Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=chalmers.se; Received: from GVYP280MB0365.SWEP280.PROD.OUTLOOK.COM...
@ruifengx Would you be willing to submit a PR that fixes the problem, e.g. by shipping a powershell script instead of the .bat?
The current content of the script is this one: https://github.com/agda/agda/blob/c0c969c661c6f2513151b6655f54e0fd99edb98d/.github/install_agda_user.bat#L1-L18 Since the `Agda_datadir` variable needs no longer be set to run agda (from 2.8.0 up), this script might become entirely...
Summoning @L-TChen as the author of these scripts to weigh in his opinion...
I am still a bit clueless on this issue because I do not really understand how the dists generated by our deploy script are supposed to be used. - Who...