Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] big.ml

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] big.ml


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page