[Agda-dev] Unification, elaboration

[Bas Spitters]

As promised, the new unification in Coq:
http://www.pps.univ-paris-diderot.fr/~sozeau/research/publications/drafts/unif.pdf
https://github.com/unicoq/unicoq

but a different elaboration algorithm is implemented in lean:
https://leanprover.github.io/files/system.pdf

I've read both papers, but I don't claim to have any definitive advice on
which option should be chosen for agda.



Regarding package managers. Coq is now moving to opam:
http://coq-blog.clarus.me/use-opam-for-coq.html
http://coq-blog.clarus.me/make-a-coq-package.html
http://coq-blog.clarus.me/a-bench-system-for-the-coq-packages.html
https://coq-bench.github.io/

There is quite a lot of discussion about this. It is not perfect, but it
allows me to conveniently switch between Coq 8.4 and Coq-HoTT. Moreover,
both we and the coq-dev get early warnings when something breaks.

Bas
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150603/ded90aa2/attachment.html