mostly cosmetic changes #9

gmalecha · 2018-06-29T15:04:56Z

What do you guys think about this change? Personally, I like the theories directory and I'd like to package this up as an opam and/or nix package so that it is easily installed.

theories directory. This seems like the common practice in Coq projects (just like src directories are common in other languages).
use coq_makefile for building, gets us a standard install target as well as documentation and is common practice.
fix all deprecation warnings in Coq 8.8, might not be backwards compatible

- theories directory (standard Coq projects) - use coq_makefile for building > gets us a standard `install` target - fix all deprecation warnings in coq 8.8 > note: might not be backwards compatible

samuelgruetter · 2018-06-29T16:34:16Z

There are three reasons why I didn't use coq_makefile:

I don't understand coq_makefile and have never used it before.
coqdep is invoked once per file, which becomes really slow on projects with many files. It's much faster to invoke coqdep just once, with all files as command line arguments (or 2 to 3 times, depending on max command line length).
I don't want to manually maintain a _CoqProject file listing all .v files.

I guess 1) should be easy to address (I hope 😉), I don't know about 2) but it should not be too much of a concern for this repo because it doesn't have many files, and 3) could probably be automated, is there a standard way to to this?

If we can address these three concerns to a reasonable extent, I'd be happy to merge this.

And thanks for fixing the deprecation warnings!

CC'ing @JasonGross and @vmurali because they use bbv in fiat-crypto and kami, respectively.

andres-erbsen · 2018-06-29T16:55:38Z

👍 and thanks to fixing warnings and moving code to a subdirectory, no opinion on coq_makefile -- I also have only used it in cargo-cult fashion, asking @JasonGross to deal with anything that breaks.

gmalecha · 2018-06-29T22:24:14Z

@samuelgruetter To your point 2, I believe this has changed. It seems to get all the dependencies via the following command:

"coqdep" -dyndep var -f _CoqProject   > ".coqdeps.d" || ( RV=$?; rm -f ".coqdeps.d"; exit $RV )

Personally, I like the list because it ensures that your build doesn't rely on any files that you aren't checking in.

samuelgruetter · 2018-06-30T13:39:24Z

Before making claim 2), I did actually bother to checkout your branch and run make, but I was using Coq 8.7.2 🙈 Now I upgraded to Coq 8.8.0, and indeed, coqdep is only called once.

Regarding 3), I'll just add an update_CoqProject makefile target once I need it.

So I'll merge this, thanks @gmalecha!

vmurali · 2018-07-03T17:13:17Z

Looks like I didn't realize this affects all the projects using bbv :(

In my setup, my _CoqProject using bbv has the following:

-R . Kami
-R ../bbv bbv

And inside my files (in Kami), I do "Require Import bbv/Word.".

Should I now change _CoqProject as follows?

-R . Kami
-R ../bbv/theories bbv

Why is this a good idea as opposed to storing the .vo files directly in the directories named after the project?

vmurali · 2018-07-03T17:15:36Z

The change didn't work. What should I do to use bbv correctly now?

gmalecha · 2018-07-04T10:09:43Z

You should do:

-Q . Kami -Q ../bbv/theories bbv You can use -R as well, but it isn't recommended. Using -Q requires that you write bbv.Xxx rather than just Xxx. Inside your files, do Require Import bbv.Xxx. If it doesn't work, then what is the error message?

On Tue, Jul 3, 2018, 1:15 PM Murali Vijayaraghavan ***@***.***> wrote: The change didn't work. What should I do to use bbv correctly now? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#9 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AASlV0CxcFXuYXMynMDVQiRHDTNlmbWwks5uC6a4gaJpZM4U9LNV> .

-- - gregory malecha gmalecha.github.io

vmurali · 2018-07-04T16:43:47Z

I think the mistake was I edited just the _CoqProject file without editing the Makefile. And I was not using coq_makefile (because I don't like listing all the files in the directory, point (2) raised by Sam). This is resolved now. Regarding -Q vs -R, I use -R, but I do Require Import bbv.Xxx, after which, I use [word n] instead of [bbv.word n]. Are you saying with -R, I might have been able to do Require Import Xxx ? On Wed, Jul 4, 2018 at 3:09 AM, Gregory Malecha <notifications@github.com> wrote:

…

You should do: -Q . Kami -Q ../bbv/theories bbv You can use -R as well, but it isn't recommended. Using -Q requires that you write bbv.Xxx rather than just Xxx. Inside your files, do Require Import bbv.Xxx. If it doesn't work, then what is the error message? On Tue, Jul 3, 2018, 1:15 PM Murali Vijayaraghavan < ***@***.***> wrote: > The change didn't work. What should I do to use bbv correctly now? > > — > You are receiving this because you were mentioned. > Reply to this email directly, view it on GitHub > <#9 (comment)>, or mute > the thread > <https://github.com/notifications/unsubscribe-auth/ AASlV0CxcFXuYXMynMDVQiRHDTNlmbWwks5uC6a4gaJpZM4U9LNV> > . > -- - gregory malecha gmalecha.github.io — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#9 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAOaRWZUSAKQUFlv9VEnefN-9AAk_do_ks5uDJRngaJpZM4U9LNV> .

gmalecha · 2018-07-05T02:48:16Z

If you don't like listing all the files in the directory, you can always do something like:

_CoqProject:
  rm -f _CoqProject
  echo "-Q ... " > _CoqProject
  for x in theories/*.v; do echo $$x >> _CoqProject; done

Yes, that is the strongly discouraged semantics of -R. The reason it is discouraged is that it doesn't play very well with packages. If someone installs a package with a file XXX, you might get their XXX instead of the one in the -R path that you specified.

samuelgruetter · 2018-07-05T21:29:46Z

Just did something like what you suggested: c2afed0

gmalecha · 2018-07-05T23:09:53Z

Oh... that seems like a step in the wrong direction to me. Can we change it back? Providing a script to generate the file is fine, but it shouldn't be necessary.

vmurali · 2018-07-06T03:52:41Z

I think the right solution is to ask for a feature request (I don't actually know who is responsible for _CoqProject format, etc).

JasonGross · 2018-07-06T04:00:48Z

I think the right solution is to ask for a feature request

What would be the feature you're requesting?

vmurali · 2018-07-06T04:15:18Z

A flag that automatically includes all the files in the directory. Say the flag is "-P"

_CoqProject:
-P theories bbv

This should automatically include all the files inside theories directory, so that

"Require Import bbv.Word.", etc. should import the definitions in theories/Word.v, respectively, as opposed to listing all the necessary files manually.

JasonGross · 2018-07-06T04:27:29Z

No, I think this is not a reasonable feature to ask for, because

It is already the case that you do not need to list any files to have Require Import bbv.Word work fine if you have -R theories bbv or -Q theories bbv, in PG and in CoqIDE. (PG and CoqIDE completely ignore the listing of .v files in _CoqProject, I believe; I think it's only there for coq_makefile.)
I think it is unreasonable to have coq_makefile issue a rule that has the Makefile regenerate itself whenever the directory tree listing of .v files has changed. That requires a great deal of Makefile magic (the only way I can think of is to record find . -name "*.v" in a file and diff that against the the current value and rebuild the Makefile if it changes), and seems like a mis-feature.

If you want to have to not manually list files, then you can build your Makefile via something like

Makefile.coq:
        $(COQBIN)coq_makefile -o Makefile.coq -f _CoqProject `find . -name "*.v"`

JasonGross · 2018-07-06T04:35:17Z

@samuelgruetter You might want to check out the update-_CoqProject rule in fiat-crypto; we have _CoqProject version-controlled, and also have a target to regenerate it when we add a new file:
https://github.com/mit-plv/fiat-crypto/blob/2a7c3b95ea4fe28a6c4cd1c5b12e3bdbb6b75204/Makefile#L59-L61

You could use something like

SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq

.PHONY: update-_CoqProject
update-_CoqProject::
	(echo '-R theories bbv'; (git ls-files 'theories/*.v' | $(SORT_COQPROJECT))) > _CoqProject

samuelgruetter · 2018-07-06T10:25:18Z

Just curious, in what way is your SORT_COQPROJECT better than plain sort?

gmalecha · 2018-07-06T11:58:15Z

I like that proposal, no opinion on the implementation of sort.

vmurali · 2018-07-06T15:39:46Z

This Makefile seems to work. This can of course be made more generic by parsing getting all the directories listed in _CoqProject (under -Q or -R) instead of manually setting up VS for every directory. This way, the Makefile takes care of dependencies when a new file is added, and doesn't recompile already compiled files. (_CoqProject does not contain all the files in it.)

VS:=$(wildcard .v)
VS+=$(wildcard Lib/.v)

.PHONY: coq src clean

ARGS := $(shell cat _CoqProject)

coq: Makefile.coq.all
$(MAKE) -f Makefile.coq.all

Makefile.coq.all: Makefile $(VS)
$(COQBIN)coq_makefile $(ARGS) $(VS) -o Makefile.coq.all

src: Makefile.coq.src
$(MAKE) -f Makefile.coq.src

Makefile.coq.src: Makefile $(VS)
$(COQBIN)coq_makefile $(ARGS) $(VS) -o Makefile.coq.src

clean:: Makefile.coq.all Makefile.coq.src
$(MAKE) -f Makefile.coq.all clean || $(MAKE) -f Makefile.coq.src clean
rm -f /.v.d /.glob /.vo /~ *~
rm -f *.hi *.o
rm -f Makefile.coq.all
rm -f Makefile.coq.src

JasonGross · 2018-07-06T20:07:13Z

ARGS := $(shell cat _CoqProject)

I think you can mix -f _CoqProject with passing the list of .v files on the command line to coq_makefile. Why not just do that?

samuelgruetter · 2018-07-10T16:30:06Z

@vmurali why do you want to have both a Makefile.coq.all and a Makefile.coq.src?
Otherwise this Makefile (with @JasonGross's fix) looks fine to me and would be worth a PR!

vmurali · 2018-07-10T16:52:27Z

OK I will take care of the current issues in the Makefile (non-use of _CoqProject, redundant definitions, etc) and if they work for my other repositories, I will make a PR.

…

On Tue, Jul 10, 2018 at 9:30 AM, Samuel Gruetter ***@***.***> wrote: @vmurali <https://github.com/vmurali> why do you want to have both a Makefile.coq.all and a Makefile.coq.src? Otherwise this Makefile (with @JasonGross <https://github.com/JasonGross>'s fix) looks fine to me and would be worth a PR! — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#9 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAOaRTAmAwSpHzRmY7oYdxkvsgZ75bTlks5uFNaPgaJpZM4U9LNV> .

gmalecha added 3 commits June 29, 2018 10:44

mostly cosmetic changes

5c1d6c6

- theories directory (standard Coq projects) - use coq_makefile for building > gets us a standard `install` target - fix all deprecation warnings in coq 8.8 > note: might not be backwards compatible

fixing the documentation target.

ed530b5

updating print_assumptions

0b13bf6

samuelgruetter merged commit fd267a7 into mit-plv:master Jun 30, 2018

samuelgruetter mentioned this pull request Jun 30, 2018

bbv makes it impossible to use $ as a prefix printing notation without parentheses #5

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

mostly cosmetic changes #9

mostly cosmetic changes #9

gmalecha commented Jun 29, 2018

samuelgruetter commented Jun 29, 2018

andres-erbsen commented Jun 29, 2018

gmalecha commented Jun 29, 2018

samuelgruetter commented Jun 30, 2018

vmurali commented Jul 3, 2018 •

edited

Loading

vmurali commented Jul 3, 2018

gmalecha commented Jul 4, 2018 via email

vmurali commented Jul 4, 2018 via email

gmalecha commented Jul 5, 2018

samuelgruetter commented Jul 5, 2018

gmalecha commented Jul 5, 2018

vmurali commented Jul 6, 2018

JasonGross commented Jul 6, 2018

vmurali commented Jul 6, 2018 •

edited

Loading

JasonGross commented Jul 6, 2018 •

edited

Loading

JasonGross commented Jul 6, 2018 •

edited

Loading

samuelgruetter commented Jul 6, 2018

gmalecha commented Jul 6, 2018

vmurali commented Jul 6, 2018

JasonGross commented Jul 6, 2018

samuelgruetter commented Jul 10, 2018

vmurali commented Jul 10, 2018 via email

mostly cosmetic changes #9

mostly cosmetic changes #9

Conversation

gmalecha commented Jun 29, 2018

samuelgruetter commented Jun 29, 2018

andres-erbsen commented Jun 29, 2018

gmalecha commented Jun 29, 2018

samuelgruetter commented Jun 30, 2018

vmurali commented Jul 3, 2018 • edited Loading

vmurali commented Jul 3, 2018

gmalecha commented Jul 4, 2018 via email

vmurali commented Jul 4, 2018 via email

gmalecha commented Jul 5, 2018

samuelgruetter commented Jul 5, 2018

gmalecha commented Jul 5, 2018

vmurali commented Jul 6, 2018

JasonGross commented Jul 6, 2018

vmurali commented Jul 6, 2018 • edited Loading

JasonGross commented Jul 6, 2018 • edited Loading

JasonGross commented Jul 6, 2018 • edited Loading

samuelgruetter commented Jul 6, 2018

gmalecha commented Jul 6, 2018

vmurali commented Jul 6, 2018

JasonGross commented Jul 6, 2018

samuelgruetter commented Jul 10, 2018

vmurali commented Jul 10, 2018 via email

vmurali commented Jul 3, 2018 •

edited

Loading

vmurali commented Jul 6, 2018 •

edited

Loading

JasonGross commented Jul 6, 2018 •

edited

Loading

JasonGross commented Jul 6, 2018 •

edited

Loading