coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Enrico Tassi <enrico.tassi AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] big.ml
- Date: Tue, 9 Oct 2018 15:07:15 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
- Ironport-phdr: 9a23:9OAAkxbEDEA1xRFPBa4LPkP/LSx+4OfEezUN459isYplN5qZoM+8bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA38G/ZlNF+gqFVoB2uuxNw3ozbb4+OOfpiYq/QZ88WSXZbU8pPUSFKH4Oyb5EID+oEJetWoI/9p0EPrRSiAgmnGf3hxSVThn/t3K0xzuMsHh/A3Aw6HtIBrHPUoM/pNKgISuC116jIwC7Cb/NQwzf96ZLHfgovofGWRL99d9fax0coFwPAlFqQqIrlMiua1uQMr2ib7/dgWvm1h2E7rAFxpz6izdovhInRno8Yzl/J+T9nzIs7P9G1SUp2bcS5HJdOtSyWL5Z6T80hTm1yvCs3y6cKtYCncCQW0pgqxx/SZvqaeIaS+B3jTvyeITJgiXJlZr2/gxGy/FCuyuLiSsm0zEtKrixZktbWrHwN0AbT6sefRvt8+EeuxyqP2hjX5+xLO0w4i6TWJ4Qgz7M0jJYfrFrPEy3ulEXzlqCWd0Ek+uay6+TgZ7XrvpCcOJVuig7gKaQjgcK/DvokMggSQmib//i826f58U3+WrVKgeU6krPFv5DCOcQbuqm5DhdJ3YYk8hazFiup0NAFnXYcN19FYxKGj43xO17UOvz4DPG/g06tkDhx3fzGMKfhUd3xKS3Il66kdrJg4WZdzhAyxJZR/cF6ELYEdd/1QE76s5TkBwQiMkTgzuD9Cd56kJ8XQnmOKq6fKqLb91GSsLF8a9KQbZMY7W6uY8Mu4OTj2CdgyA0tOJKx1J5SU0iWW/FvIkGXe33p24tTH2oWohc4UOWsj0eNA2YKOySCGpkk7zR+M7qISJ/ZT9n10r2HxiayWJNMNDgfVwK8VEzwfoDBYM8iLSKfJsg4zm4KWKS9Vok93FeprgCok7c=
On Mon, Oct 08, 2018 at 11:09:35PM -0700, Vadim Zaliva wrote:
> Am I supposed to copy big.ml from Coq source tree to my project?
As of today, this is the only solution :-/
You may also try to give a look at
https://github.com/coq/coq/pull/8252
that will let you write
ocamlfind opt -package coq.extraction.runtime yourcode.ml
in order to compile your extracted code.
The PR is promising, but seems to need some more work. Showing your
interest in there may help motivating the authors.
Best,
--
Enrico Tassi
- [Coq-Club] big.ml, Vadim Zaliva, 10/09/2018
- Re: [Coq-Club] big.ml, Enrico Tassi, 10/09/2018
- Re: [Coq-Club] big.ml, Ana, 10/10/2018
- Re: [Coq-Club] big.ml, Enrico Tassi, 10/09/2018
Archive powered by MHonArc 2.6.18.