mostly cosmetic changes

[gmalecha]

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

[samuelgruetter]

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

1. I don't understand coq_makefile and have never used it before.
2. 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).
3. I don't want to manually maintain a _CoqProject file listing all .v files.

I guess 1) should be easy to address (I hope :wink:), 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]

:+1: 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]

@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]

Before making claim 2), I did actually bother to checkout your branch and run make, but I was using Coq 8.7.2 :see_no_evil: 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]

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]

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

[gmalecha]

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 notifications@github.com 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 https://github.com/mit-plv/bbv/pull/9#issuecomment-402230423, or mute the thread https://github.com/notifications/unsubscribe-auth/AASlV0CxcFXuYXMynMDVQiRHDTNlmbWwks5uC6a4gaJpZM4U9LNV .

--

• gregory malecha gmalecha.github.io

[vmurali]

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 < notifications@github.com> 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 https://github.com/mit-plv/bbv/pull/9#issuecomment-402230423, 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 https://github.com/mit-plv/bbv/pull/9#issuecomment-402432978, or mute the thread https://github.com/notifications/unsubscribe-auth/AAOaRWZUSAKQUFlv9VEnefN-9AAk_do_ks5uDJRngaJpZM4U9LNV .

[gmalecha]

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]

Just did something like what you suggested: https://github.com/mit-plv/bbv/commit/c2afed082b581dbed17575147af8015fcf83cf3b

[gmalecha]

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]

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]

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

What would be the feature you're requesting?

[vmurali]

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]

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

1. 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.)
2. 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]

@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]

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

[gmalecha]

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

[vmurali]

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]

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]

@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]

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 notifications@github.com 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 https://github.com/mit-plv/bbv/pull/9#issuecomment-403885433, or mute the thread https://github.com/notifications/unsubscribe-auth/AAOaRTAmAwSpHzRmY7oYdxkvsgZ75bTlks5uFNaPgaJpZM4U9LNV .