coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] scons equivalent of coq_makefile

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] scons equivalent of coq_makefile
Date: Tue, 8 Sep 2020 21:03:27 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f174.google.com
Ironport-phdr: 9a23:uuq9rxTQaXwfoCzC1GeUtlABi9psv+yvbD5Q0YIujvd0So/mwa6ybR2N2/xhgRfzUJnB7Loc0qyK6v6mADZcqsbY+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi3oAnLq8Uan4RvJqkyxxfUv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBNxw4HWYI+bOvlwcL7Dc9wGXmdORNpdWjZbD4+gc4cCDewMNvtYoYnnoFsOqAOzCBW3C+Pvyz9InX/20rM50+88DQzG2hYvH9QTv3/Jq9j6LrwdUeC0zKnTzTXMcfBW1S3n54jOaB8hp+yDUahxccrQ1UkvGBjIjlqVqYP/PjOV0v4BvHSc7+plTO+ijXMspA5trDa13MgslpXJiZwPylDC7Sh0wYY4K922RUNmYtOoDZteuj2UOodoX88vTWNltScmxrACtpO2YDQHxZApyRPfavGLb4eG7wzsWeufLjp0mH1rdbSijBi89kigz/fzVsiy0FtSoSpFk8XMtnAQ1xPI8MSIVvx9/kKn1D2S1A7T8vlJLV4omaffMZIswb49moAOvUnCHyL6glj6ga2Ze0gi5+Om8f7oYq/8qZ+ZL4J0ih/xMqApmsGnBOQ3KAkOX2yC9eS90L3v4FT1QLtXgvA0naTVqp/aJcMcpq62Bw9azJwv5Aq4DzejyNgYnH8HI0xZeB+fkYTlJ1XDLOr7APq/mVigjTZmyvHcMrH8AJjAIWDPkLL7crZ8705cxhAzzdda559MEL4OO/LzWk7qtNzYEBA5MBa4zPzhCNpn0IMRRHiDAq6YMKPOvl+F/e0vI+yWa48UvDbxMeQq5/nrjXMhg18SYbGp3YcLaHC/BvlpP0KZYWP1jtgdFWcKoxExQffxiFyCVD5Tf2y9U7g95jE9EoKmDJ3MSpqjgLybj2+HGchdYXkDAVSRGz+8fIKdHvwIdSi6I8l7kzVCW6L3GKE70hT7nQX6yqFnI+mc0ysRs56rgNF/5+zIlRwxszVyBsKRlWCMU25ckWYBRjtw16d69x8ugmyf2LR11qQLXedY4OlEB19jaMzsitdiAtW3YTrvO9eETFH8HIejCDA1C9M1mpoAOhkhXdqliR/H0myhBLpHz+XaVqxxybrV2j3KH+g4zn/H0Kc7iFx/G5lAMGSnguh08A2BXteVwXXcrL6jcOEn5ACI7H2KlDPcs0RRUQo2WqLADygS

Regarding coqdep, the coqdep rule for a theory in dune depends on all .v files for that theory. So indeed the behavior should be like coq_makefile’s.

It doesn't have to be that eager.

All Coq projects I have worked with have a situation (I think) where there is a "one to one correspondence" between logical paths and physical paths: for each fully qualified logical module name, there exists a unique physical path that matches it based on the -Q/COQPATH directives.

On a day to day basis, that very property enables us human Coq programmers to look at a logical module name and be able to locate the corresponding .v file in the file system.

Under such typical -Q/COQPATH configurations, coqdep could therefore compute where the physical path for a logical path should be and thereby generate the appropriate dependency graph without needing to auto generate all the .v files. This is what I implemented here: https://github.com/coq/coq/pull/12108

Re: [Coq-Club] scons equivalent of coq_makefile, Abhishek Anand, 09/09/2020