[Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!

[darais at cs.umd.edu]

Hi Andreas,

No Breakage.

I have a ~10.5k lines and growing Agda development for mechanizing Galois
connections and proofs by abstract interpretation, including calculational
abstract interpretation. (See our draft[1] which includes Agda details. We have
a better draft coming out momentarily; ping me if interested.) The
calculational style in particular uses lots of Agda computation during
type-checking. I'm not a heavy user of `rewrite` and `with` at the moment.
There are ~100 occurrences of `rewrite` and ~150 of `with` in my development.

[1]: http://arxiv.org/abs/1507.03559

---

Some notes on installing the branch in case anybody else gets stuck...

Make sure you have updated your hackage list with `cabal update`.

I was unsuccessful in building the branch from a fresh cabal sandbox using
cpphs-1.19.3. Bounds are stated "'cpphs' version >=1.19 && <1.20 is required”
and 1.19.3 is automatically installed since it's the latest on hackage. The
error I get is "The program 'cpphs' version >=1.19 && <1.20 is required but it
could not be found." and if I point to it explicitly with
"--with-cpp=/.../.cabal-sandbox/bin/cpphs-2.4.2.5" I get "ghc: could not
execute: cpphs". I was able to install successfully after downgrading to
1.19.2. To downgrade I did the following from a cabal sandbox, which seemed to
do the trick (because haskell-src-exts is the only dependency):
  
    cabal exec -- ghc-pkg unregister haskell-src-exts-1.16.0.1
    cabal exec -- ghc-pkg unregister cpphs-1.19.3 
    cabal install cpphs-1.19.2
    make install-bin
  
At some point I added the cabal sandbox bin folder (./.cabal-sandbox/bin) to my
path before trying this, so there is a small chance that is required too...

Thanks for Agda!

Best,
David

> Date: Thu, 19 Nov 2015 14:16:52 +0100
> From: Andreas Abel <andreas.abel at ifi.lmu.de>
> Subject: [Agda] More aggressive `with`: Please check your Agda-2.4.2
> 	developments!
> To: Agda List <agda at lists.chalmers.se>
> Message-ID: <564DCBC4.2000608 at ifi.lmu.de>
> Content-Type: text/plain; charset=utf-8; format=flowed
> 
> Dear Agda users and developers,
> 
> please check your larger Agda-2.4.2 developments with the version at
> 
>   https://github.com/andreasabel/agda-issue-1692/tree/maint-2.4.2
> 
> You can get it with
> 
>   git clone https://github.com/andreasabel/agda-issue-1692.git
>   cd agda-issue-1692
>   git checkout maint-2.4.2
>   make install-bin
> 
> This version is making `with` more agressive and hopefully more 
> intuitive (at least it removes the stumbling block reported in issue #1692).
> 
> The change is not fully backwards compatible. However, the breakage 
> should be small. Nothing broke for the std-lib. Only a single test case 
> broke, which uses with on a function argument (a variable):
> https://github.com/agda/agda/blob/master/test/lib-succeed/Issue846/DivModUtils.agda#L99
> The breakage was easy to fix, the new `with` is simpler: the `with` on 
> the variable could be removed.
> 
> Please check the amount of breakage on your Agda developments and report 
> back, with self-contained test-cases (e.g. as tar-balls and repo links) on
> 
>   https://github.com/agda/agda/issues/1692
> 
> This let's me evaluate whether this commit can go into the maintenance 
> version or not (in case the breakage is too big).
> 
> Response time: 5 work days.
> 
> Cheers,
> Andreas
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
> 
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/