coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] scons equivalent of coq_makefile

From: Gregory Malecha <gregory AT bedrocksystems.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] scons equivalent of coq_makefile
Date: Mon, 31 Aug 2020 13:21:59 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gregory AT bedrocksystems.com; spf=None smtp.mailfrom=gregory AT bedrocksystems.com; spf=None smtp.helo=postmaster AT mail-pj1-f48.google.com
Ironport-phdr: 9a23:KewJiBccMTMnK8MaaY0KJTuxlGMj4u6mDksu8pMizoh2WeGdxcW4bB7h7PlgxGXEQZ/co6odzbaP7ea5AzBLsc/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRS7oR/MusUIjoZuJaU8xgbUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+uqBJ/zIzUbo+bN/RwY73Tcs8BSGVbQspcTTZMDp+gY4YNCecKIOZWr5P6p1sLtRawBBOsC/3gyj9PnH/33bAx3eM7HgHCwgMvA9IOv27Jp9jyO6cSS/66zKbPzTXZb/Jbwizy55bVfRA7pvGDQbFwcdHRyEk0CwPKkFCQqZf/MzyJ0eQNtnGW4ux9Xu2gl2ApsRt+oiSzxsgykInJgJoYx0zL+yhl3Is5OdO2RU1lbNCqFJZdqi6UO5d5T84iQWxluyY0x7MYtJO0fiUHzJsqyhDQZfCZfIWE/wzvWeKSLDp+mXlrdrW/hxOo/kihzO3xTsi00FBQripEiNbArH4N1wbL5sidVPRy5Fqu2SqP1w/N9+5EJlw7lbHBJ54gxb48joccsUXYHiDqn0X2kbWWdl469eSy5OTneLLmpoKEN4JylwrwMbwul9ShDegkNgUCRWuW9OSm2LH94EH0Qa9Gg/I1n6TfrZvUP94UprSjDA9Qyosj6wiwDzOh0NkAmHkINlNFeBaeg4jxOVHCPen0DfmwjlmvijtryPfGPrruApXJMHfPiqvufbF460JEyQozy85Q545MB70fPP7+XlX9ud/YAxMjLQC43ufqBM9y244dQW6PB7WWMKLWsV+G/OIvJOyMaZcauDbnNfcl6PnujWU5mFIGZqamw4YYaGq/Hvt6IEWZenrtgswdEWgUuwo+V/bmh0GFUT5Wf3qyRb4z5iknCIK6CofOXpyigLuY3CuiApJWYn1GBUuXHHfzd4SEXu8MZziILs9glDwET7mhRJU72RGgrg+pg4Zge+HT42gTsY/p/Nlz/eza0x8ophJuCMHI/HuAQGZujystTjs716B26Rhy0FqM1rJpq/ZVGcZU7PBSQxwmOJvHied9DoahCUr6Yt6VRQP+EZ2dCjYrQ4dpmo5cUwNGA9ynyyv78W+vCr4RmaaMAcZsoKjR02L2LMVm2m3a2aw6yVIhR5kXbDH0tutE7wHWQrXxvQCBja/wLfYW0SLX82yA1nuVoExdS0h7VqCXBSlCNHuTlszw4wb5d5HrCbkjNVEcm8uLK68Pct+wyFsaFLHsP9PRZ2/3kGC1V06F

Does dune have a way to run pre-processors? For example, we have a tool, cpp2v, that takes a C++ file and generates a Coq file. I haven't found a way to get dune to do this for me.

On Sat, Aug 29, 2020 at 5:50 AM Théo Zimmermann <theo AT irif.fr> wrote:

Dear Abhishek,

If you are looking for a way to get away from the limitations of make,
why not try the experimental Dune support for Coq instead?

See:
- https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project-with-dune
- https://dune.readthedocs.io/en/stable/dune-files.html#coq-theory
- https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20

Cheers,
Théo

Le jeu. 20 août 2020 à 21:37, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> a écrit :
>
> Has someone written a tool to produce scons declarations (SConstruct) from a _CoqProject?
> I find it advantageous over make, especially in cross-server CI settings, because it uses hashes instead of timestamps to decide whether to rebuild a .vo file.

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING

[Coq-Club] scons equivalent of coq_makefile, Abhishek Anand, 08/20/2020
- Re: [Coq-Club] scons equivalent of coq_makefile, Théo Zimmermann, 08/29/2020
  - Re: [Coq-Club] scons equivalent of coq_makefile, Clément Pit-Claudel, 08/30/2020
  - Re: [Coq-Club] scons equivalent of coq_makefile, Gregory Malecha, 08/31/2020
    - Re: [Coq-Club] scons equivalent of coq_makefile, Rudi Grinberg, 08/31/2020
      - Re: [Coq-Club] scons equivalent of coq_makefile, Abhishek Anand, 08/31/2020
        
        Re: [Coq-Club] scons equivalent of coq_makefile, Rudi Grinberg, 08/31/2020