coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Add a new extraction language in a project?

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Add a new extraction language in a project?
Date: Tue, 01 Mar 2016 07:15:41 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f177.google.com
Ironport-phdr: 9a23:JqwbahVdjHZwKHtQMJZw4quRMgzV8LGtZVwlr6E/grcLSJyIuqrYZhyBt8tkgFKBZ4jH8fUM07OQ6PC/HzNYqsnY+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVPF0D22P1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtUERSmEHrh0dSSrC7BeyYZb8vS/3p6A1jCudPcvpZbY5Rj2486ZwQRnzziwAMmhq3nvQj5k6rqVbplqephFwx4PFKsnBNv1+eLz1e94FTHBdX91YUTcHCYS5OdhcR9EdNPpV+tGu72AFqgGzUFGh
Organization: New Artisans LLC

Is it possible to create a new extraction language plugin, and build and load
it within a single project? That is, I'd like to add a new language target,
but without requiring a patch and rebuild of the Coq sources. Is this
possible?

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Add a new extraction language in a project?, John Wiegley, 03/01/2016