Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Garagedoor opens #1369

Merged
merged 24 commits into from
Sep 30, 2022
Merged

Garagedoor opens #1369

merged 24 commits into from
Sep 30, 2022

Conversation

andres-erbsen
Copy link
Contributor

No description provided.

@andres-erbsen andres-erbsen marked this pull request as ready for review September 5, 2022 20:47
@andres-erbsen
Copy link
Contributor Author

I just merged the dependencies; this is ready to merge if it passes.

@andres-erbsen
Copy link
Contributor Author

Error: Cannot find a physical path bound to logical path bedrock2Examples.LAN9250.
Probably the thing to do here is to create another build category that depends on bedrock2 and rupicola examples...

@andres-erbsen andres-erbsen force-pushed the garagedoor-opens branch 2 times, most recently from 7567ddd to 3d9c3dd Compare September 12, 2022 23:53
@andres-erbsen
Copy link
Contributor Author

8.14:

File "/Users/runner/work/fiat-crypto/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples/memmove.v", line 190, characters 12-63:
Error: No such bound variable m (possible names are: k, v1, v2 and m1).

@andres-erbsen
Copy link
Contributor Author

andres-erbsen commented Sep 23, 2022 •
edited

@JasonGross please consider whether it's worth getting this to build on 8.14 or whether we're likely enough to drop it anyway. My recollection of build discussion:

  • make clean does not remove .vo files from submodules (probably because these .v files are not listed in _CoqProject)
  • .v files not wanted in _CoqProject can be outside src
  • _CoqProject generation (and the rest of the Makefile) should work without .git
  • we want to be able to check locally that .v-files in _CoqProject are in git to avoid CI surprises, and enable this check by default. I think this should be a separate phony target from _CoqProject generation.

I'm willing to implement these if you expect you'd find the result acceptable. wdyt?

@JasonGross
Copy link
Collaborator

I think we're going to drop 8.14, to get adequate Ltac2 support if nothing else, so you should just cherry-pick the first two commits of #1361

I think actually the Makefile already works without .git by falling back to find, though I could be misremembering. I continue to be slightly sad about, e.g., having to pick a different directory to run the bug minimizer in. If we already fall back to find, feel free to stop checking in the generated files. Otherwise I'm happy to add a find fallback.

JasonGross
JasonGross reviewed Sep 23, 2022
View reviewed changes
.dir-locals.el
@@ -1,23 +0,0 @@
((coq-mode . ((eval . (let* ((project-root (locate-dominating-file buffer-file-name "_CoqProject"))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why delete this?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's redundant as Makefile-generated _CoqProject already passes -Q with these directories.

@JasonGross
Copy link
Collaborator

Hmmm, I guess we don't fallback to find. Thoughts on using git when it's available and otherwise find?

@andres-erbsen andres-erbsen force-pushed the garagedoor-opens branch 4 times, most recently from 3c26bd8 to 2c0aef6 Compare September 29, 2022 21:17
@andres-erbsen andres-erbsen mentioned this pull request Sep 29, 2022
Closed
@andres-erbsen
Copy link
Contributor Author

make: *** No rule to make target 'rupicola/src/Rupicola/Lib/Tactics.vo', needed by 'src/Assembly/WithBedrock/Proofs.vo'. Stop.
I vaguely remember @samuelgruetter had to do some hacks to get -Q to work on Windows...

@samuelgruetter
Copy link
Contributor

I vaguely remember @samuelgruetter had to do some hacks to get -Q to work on Windows...

I don't remember inventing or using any hacks for Windows myself, but here's one by @JasonGross that might be relevant:

fiat-crypto/Makefile

Lines 438 to 442 in 64aa176

ifneq ($(filter /cygdrive/%,$(CURDIR)),)
CURDIR_SAFE := $(shell cygpath -m "$(CURDIR)")
else
CURDIR_SAFE := $(CURDIR)
endif

@andres-erbsen
Copy link
Contributor Author

Yeah, looks possible that it worked before I just broke it when cleaning up the Makefile...

@andres-erbsen andres-erbsen enabled auto-merge (rebase) September 30, 2022 02:35
JasonGross
JasonGross reviewed Sep 30, 2022
View reviewed changes
Makefile
Comment on lines -143 to -158
FORCE_BEDROCK2?=
ifneq (,$(filter 8.11% 8.12% 8.13%,$(COQ_VERSION)))
ifneq ($(SKIP_BEDROCK2),1)
$(warning Coq version $(COQ_VERSION) is older than the minimum bedrock2 Coq version of 8.14)
ifeq ($(FORCE_BEDROCK2),1)
$(warning Building bedrock2 code anyway because FORCE_BEDROCK2=$(FORCE_BEDROCK2))
else
ifeq ($(SKIP_BEDROCK2),)
SKIP_BEDROCK2=1
else
$(error Cannot build bedrock2! Pass FORCE_BEDROCK2=1 to override this error and build anyway, or pass SKIP_BEDROCK2=1 (instead of SKIP_BEDROCK2=$(SKIP_BEDROCK2)) to skip bedrock2)
endif
endif
endif
endif

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why remove this? It seems useful to be able to easily desync the bedrock2 minimal version from the fiat-crypto minimal version, no?

Makefile
@@ -580,7 +542,7 @@ endif

Makefile.coq: Makefile _CoqProject
$(SHOW)'COQ_MAKEFILE -f _CoqProject > $@'
$(HIDE)$(COQBIN)coq_makefile -f _CoqProject INSTALLDEFAULTROOT = $(INSTALLDEFAULTROOT) -o Makefile-coq && cat Makefile-coq | sed 's/^printenv:/printenv::/g; s/^printenv:::/printenv::/g; s/^all:/all-old:/g; s/^validate:/validate-vo:/g; s/^.PHONY: validate/.PHONY: validate-vo/g' > $@ && rm -f Makefile-coq
$(HIDE)$(COQBIN)coq_makefile -f _CoqProject INSTALLDEFAULTROOT = $(INSTALLDEFAULTROOT) -o $@
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that this will result in duplicated targets for Makefile.coq. idk how bad this is

@JasonGross
Copy link
Collaborator

make: *** No rule to make target 'rupicola/src/Rupicola/Lib/Tactics.vo', needed by 'src/Assembly/WithBedrock/Proofs.vo'. Stop. I vaguely remember @samuelgruetter had to do some hacks to get -Q to work on Windows...

This is still an issue. I think the problem is that deps is for some reason not building this .vo file.

(What's the reason to update the Makefile logic in the same PR as updating code?)

JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Sep 30, 2022
@JasonGross
Update src/Assembly to work with new rupicola/coqutil
4e798e3 
Lifted from mit-plv#1369
JasonGross
JasonGross reviewed Sep 30, 2022
View reviewed changes
Makefile Show resolved Hide resolved
JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Sep 30, 2022
@JasonGross
Drop Nsatz version-specific hacks
e55767e 
Mostly lifted from mit-plv#1369

Now that we require Coq >= 8.15, we no longer need to do
version-specific nsatz-tactic hacking.
@JasonGross JasonGross mentioned this pull request Sep 30, 2022
Closed
JasonGross added a commit that referenced this pull request Sep 30, 2022
@JasonGross
Update src/Assembly to work with new rupicola/coqutil
bfa4616 
Lifted from #1369
andres-erbsen and others added 18 commits September 30, 2022 17:22
@andres-erbsen @JasonGross
garage door opener draft (replies with something)
79355da
@andres-erbsen @JasonGross
garagedoor opens
c316a24
@samuelgruetter @JasonGross
specify non-external dependencies using -Q instead of COQPATH
54982a3 
This leads to .Makefile-coq.d containing also dependencies on the
files in submodules, so if a file in the rupicola or bedrock2
submodule is modified, fiat-crypto's make knows which files in
fiat-crypto it has to recompile because of the submodule changes.
@andres-erbsen @JasonGross
use -Q in _CoqProject
2ab3721
@andres-erbsen @JasonGross
git rm .dir-locals.el
36e4b2a
@samuelgruetter @JasonGross
adapt to compiler now using list instead of SortedListString.map
cf27b9c
@samuelgruetter @JasonGross
print assembly (of compiler with improved regalloc)
3bea236
@andres-erbsen @JasonGross
bump bedrock2: memswap/memequal/memconst
d3722b6
@andres-erbsen @JasonGross
prove bedrock2 x25519 wrappers
da5f924
@andres-erbsen @JasonGross
garagedoor wire format change
c10b236
@andres-erbsen @JasonGross
Makefile: bedrock2: bedrock2_ex
0016ba0
@andres-erbsen @JasonGross
create GarageDoor.v
83b9663
@andres-erbsen @JasonGross
make partial progress on GarageDoor trace spec
c52ad2c
@andres-erbsen @JasonGross
GarageDoor: clean out easy admits
b0bd591
@andres-erbsen @JasonGross
Garagedoor: down to chacha20
5cee1ce
@andres-erbsen @JasonGross
remove git, 8.13, src/Specific from Makefile
b22a601
@andres-erbsen @JasonGross
bump bedrock2 for Windows support...
e688132
@andres-erbsen @JasonGross
stop tracking Everything.v in git
6b0cba6
@andres-erbsen andres-erbsen merged commit 7eeb403 into master Sep 30, 2022
@andres-erbsen andres-erbsen deleted the garagedoor-opens branch September 30, 2022 12:01
andres-erbsen pushed a commit that referenced this pull request Sep 30, 2022
@JasonGross @andres-erbsen
Drop Nsatz version-specific hacks
14428e0 
Mostly lifted from #1369

Now that we require Coq >= 8.15, we no longer need to do
version-specific nsatz-tactic hacking.
@JasonGross JasonGross mentioned this pull request Oct 1, 2022
Closed
2 tasks
OwenConoly pushed a commit that referenced this pull request Nov 13, 2022
@JasonGross @OwenConoly
Drop Nsatz version-specific hacks
96e369d 
Mostly lifted from #1369

Now that we require Coq >= 8.15, we no longer need to do
version-specific nsatz-tactic hacking.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JasonGross JasonGross JasonGross left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@andres-erbsen @JasonGross @samuelgruetter @talkon