Coq small fixes #1108
Coq small fixes #1108
Conversation
cmester0
force-pushed
the
coq-small-fixes
branch
5 times, most recently
from
f7cb54f to
e39e7cd
Compare
| @@ -56,3 +82,9 @@ Definition asserts (_ : unit) : unit := | |||
| end in | |||
| tt. | |||
| ''' | |||
| _CoqProject = ''' | |||
| -R ./ TODO | |||
There was a problem hiding this comment.
Add name of create instead of TODO.
| // TODO: | ||
| // fn test() { | ||
| // let add : fn(i32, i32) -> i32 = |x, y| x + y; | ||
| // let _ = (|x : &u8| { x + x })(&2); | ||
|
|
||
| // fn f<F : FnOnce() -> u8> (g: F) -> u8 { | ||
| // g() + 2 | ||
| // } | ||
|
|
||
| // f(|| { | ||
| // 23 | ||
| // }); | ||
| // // Prints "foobar". | ||
| // } |
There was a problem hiding this comment.
Support closures.
cmester0
force-pushed
the
coq-small-fixes
branch
3 times, most recently
from
e04856e to
5afea93
Compare
cmester0
changed the base branch from
main
to
coq-generic-printer-annotated-core-lib
cmester0
force-pushed
the
coq-small-fixes
branch
5 times, most recently
from
a4ab210 to
ddec63c
Compare
|
Let's look at that together to chat about CI, and merge |
|
Lasse and I are looking at that PR right now |
cmester0
force-pushed
the
coq-small-fixes
branch
from
0150344 to
ff429a0
Compare
W95Psp
force-pushed
the
coq-small-fixes
branch
from
ff429a0 to
197d1a3
Compare
| # - name: build and run coq on tests | ||
| # env: | ||
| # FILES: assert attribute-opaque enum-struct-variant | ||
| # NOT_SUPPORTED_FILES: attributes cli conditional-match constructor-as-closure cyclic-modules enum-repr even dyn functions | ||
| # run: | | ||
| # for f in $FILES; do \ | ||
| # cd hax/tests/$f && \ | ||
| # nix run . into coq && \ | ||
| # cd ../../.. | ||
| # done | ||
| # for f in $FILES; do \ | ||
| # cd hax/tests/$f/proofs/coq/extraction && \ | ||
| # nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \ | ||
| # nix-shell --packages coq coqPackages.coq-record-update --run "make" && \ | ||
| # cd ../../../../../../ | ||
| # done |
There was a problem hiding this comment.
Run Coq on (working) snapshot files. Still have to get full coverage.
|
@W95Psp The Coq code should work now. Seems to be an issue with |
|
@W95Psp please have a look at this. |
| buildPhaseCargoCommand = '' | ||
| cd examples/coverage | ||
| cargo hax into coq | ||
|
|
||
| cd proofs/coq/extraction |
There was a problem hiding this comment.
Does the cd issue originate from here? Does it fail to generate something when running cargo hax here?
|
It would be good to get this merged, the tests are nice, however, if we do not want to fix the Nix setup now, I can remove that part. Some of the features in this PR are related to the issues Andrei Listochkin is experiencing with the Coq backend. |
|
I'm looking into it |
This commit allows for a better control over name rendering. This is useful for PR #1108.
|
@cmester0 I merged main and fixed a few things. Otherwise, I think moving the test nix part to another PR that I can fix later would be great. |
W95Psp
added
the
waiting-on-author
| ((`Type n | `Const n | `Fn n), (`Trait _ | `Impl (_, `Trait, _))) -> | ||
| prefix "f" (dstr n) |
There was a problem hiding this comment.
It seems the update of how names are rendered broke the Coq naming scheme, since the trait name needs to be prepended. Changing this to
| `AssociatedItem
((`Type n | `Const n | `Fn n), (`Impl (_, `Trait, _))) ->
prefix "f" (dstr n)
| `AssociatedItem
((`Type n | `Const n | `Fn n), (`Trait (a, _))) ->
Concat (dstr a, prefix "f" (dstr n))Only half fixes the issue, as I still need to prefix the impl function name.
No description provided.