Generated rust code doesn't compile #16

womeier · 2024-03-18T23:51:33Z

I'm trying to extract the CertiCoq benchmarks to rust and run them.
The extraction succeeds for all of them, but not all of them compile.

What works

demo1, demo2, list_sum (these are fairly small)
binom (works with export RUST_MIN_STACK=1000000000 otherwise the rust compiler crashes, see rustc stackoverflow (SIGSEGV) rust-lang/rust#122715)
color (some Wasm tools have issues with the Wasm file our CertiCoq-Wasm generates for color, but no issues with the rust extraction)

What doesn't work (see compilation errors below)

vs_easy, vs_hard (seems to be the same problem)
sha_fast (seems to be a separate issue)

Rust extraction setup in one diff

see this diff

To set up yourself

clone: https://github.com/womeier/certicoqwasm/tree/rustextraction (no need to compile certicoq, the benchmarks have no dependencies other than coq-rust-extraction)
cd benchmarks && make for the extraction, runs one benchmark successfully (prints 100))
python3 run_rust_benchmarks.py, this calls cargo run for all benchmarks, which includes printing some lengthy s-expressions to stdout)

Versions

Coq: 8.17.0
MetaCoq: v1.2.1-8.17
rustc: 1.76.0 (07dca489a 2024-02-04)

coq-rust-extraction: most recent (6e72e1c)

Errors

vs easy

cargo run
   Compiling vs_easy v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/certicoqwasm-rustextraction/benchmarks/rust/vs_easy-extracted)
error: expected identifier, found keyword `loop`
    --> src/main.rs:9667:27
     |
9667 |   hint_app(hint_app({ let loop = self.alloc(std::cell::Cell::new(None));
     |                           ^^^^ expected identifier, found keyword
     |
help: escape `loop` to use it as an identifier
     |
9667 |   hint_app(hint_app({ let r#loop = self.alloc(std::cell::Cell::new(None));
     |                           ++

error: expected `{`, found `.`
    --> src/main.rs:9668:27
     |
9668 |                       loop.set(Some(
     |                       ----^ expected `{`
     |                       |
     |                       while parsing this `loop` expression

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:261:8
    |
261 |   self.Coq_PArith_BinPosDef_Pos_add()
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:258:4
    |
258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b }
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
261 |   self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */)
    |                                    ~~~~~~~~~~~~~~~~~~~~~~

error[E0308]: mismatched types
   --> src/main.rs:261:3
    |
260 | fn CertiCoq_Benchmarks_lib_vs_add_id(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> u64 {
    |                                                   ----------------------------------------- expected `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)` because of return type
261 |   self.Coq_PArith_BinPosDef_Pos_add()
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `&dyn Fn(u64) -> &dyn Fn(u64) -> u64`, found `u64`
    |
    = note: expected reference `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)`
                    found type `u64`

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:302:12
    |
302 |       self.Coq_PArith_BinPosDef_Pos_add()(
    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:258:4
    |
258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b }
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
302 |       self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */)(
    |                                        ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `u64`
   --> src/main.rs:302:7
    |
302 |         self.Coq_PArith_BinPosDef_Pos_add()(
    |         -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
    |  _______|
    | |
303 | |         p)(
    | |__________- call expression requires function

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:509:16
    |
509 |           self.Coq_PArith_BinPosDef_Pos_compare()(
    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:383:4
    |
383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering {
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
509 |           self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
    |                                                ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
   --> src/main.rs:509:11
    |
509 |             self.Coq_PArith_BinPosDef_Pos_compare()(
    |             -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
    |  ___________|
    | |
510 | |             v)(
    | |______________- call expression requires function

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:784:14
    |
784 |   match self.Coq_PArith_BinPosDef_Pos_compare()(
    |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:383:4
    |
383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering {
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
784 |   match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
    |                                              ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
   --> src/main.rs:784:9
    |
784 |     match self.Coq_PArith_BinPosDef_Pos_compare()(
    |           -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
    |  _________|
    | |
785 | |           self.CertiCoq_Benchmarks_lib_vs_clause_prio(
786 | |             cl1))(
    | |_________________- call expression requires function

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
    --> src/main.rs:2689:18
     |
2689 |       match self.Coq_PArith_BinPosDef_Pos_compare()(
     |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
     |
note: method defined here
    --> src/main.rs:383:4
     |
383  | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering {
     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
     |
2689 |       match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
     |                                                  ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
    --> src/main.rs:2689:13
     |
2689 |         match self.Coq_PArith_BinPosDef_Pos_compare()(
     |               -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
     |  _____________|
     | |
2690 | |               i)(
     | |________________- call expression requires function

error[E0308]: mismatched types
    --> src/main.rs:3765:29
     |
3762 |                             self.CertiCoq_Benchmarks_lib_vs_mergeC(
     |                                  --------------------------------- arguments to this method are incorrect
...
3765 | /                             self.Coq_Init_Datatypes_id()(
3766 | |                               ()),
     | |_________________________________^ expected `&dyn Fn(&...) -> ...`, found `&dyn Fn(())`
     |
     = note: expected reference `&dyn Fn(&CertiCoq_Benchmarks_lib_vs_expr<'_>) -> &CertiCoq_Benchmarks_lib_vs_expr<'_>`
                found reference `&dyn Fn(())`
note: method defined here
    --> src/main.rs:3658:4
     |
3658 | fn CertiCoq_Benchmarks_lib_vs_mergeC<A: Copy, B: Copy>(&'a self, A_cmp: &'a dyn Fn(A) -> &'a dyn Fn(A) -> std::cmp::Ordering, B_cmp: &'a dyn Fn(B) -> &'a dyn Fn(B) -> std::cmp::Ordering, fAB: &'a dyn Fn(A) -> B, a...
     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^                                                                                                                                                       -----------------------

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
    --> src/main.rs:6533:10
     |
6533 |     self.Coq_PArith_BinPosDef_Pos_compare()(
     |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
     |
note: method defined here
    --> src/main.rs:383:4
     |
383  | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::Ordering {
     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
     |
6533 |     self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
     |                                          ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
    --> src/main.rs:6533:5
     |
6533 |       self.Coq_PArith_BinPosDef_Pos_compare()(
     |       -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
     |  _____|
     | |
6534 | |       i)(
     | |________- call expression requires function

Some errors have detailed explanations: E0061, E0308, E0618.
For more information about an error, try `rustc --explain E0061`.
error: could not compile `vs_easy` (bin "vs_easy") due to 15 previous errors

vs hard

running: vs_hard
   Compiling vs_hard v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/certicoqwasm-rustextraction/benchmarks/rust/vs_hard-extracted)
error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:261:8
    |
261 |   self.Coq_PArith_BinPosDef_Pos_add()
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:258:4
    |
258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b }
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
261 |   self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */)
    |                                    ~~~~~~~~~~~~~~~~~~~~~~

error[E0308]: mismatched types
   --> src/main.rs:261:3
    |
260 | fn CertiCoq_Benchmarks_lib_vs_add_id(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> u6...
    |                                                   ----------------------------------------- expected `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)` because of return type
261 |   self.Coq_PArith_BinPosDef_Pos_add()
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `&dyn Fn(u64) -> &...`, found `u64`
    |
    = note: expected reference `&'a (dyn Fn(u64) -> &'a (dyn Fn(u64) -> u64 + 'a) + 'a)`
                    found type `u64`

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:302:12
    |
302 |       self.Coq_PArith_BinPosDef_Pos_add()(
    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:258:4
    |
258 | fn Coq_PArith_BinPosDef_Pos_add(&'a self, a: u64, b: u64) -> u64 { a + b }
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
302 |       self.Coq_PArith_BinPosDef_Pos_add(/* u64 */, /* u64 */)(
    |                                        ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `u64`
   --> src/main.rs:302:7
    |
302 |         self.Coq_PArith_BinPosDef_Pos_add()(
    |         -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
    |  _______|
    | |
303 | |         p)(
    | |__________- call expression requires function

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:509:16
    |
509 |           self.Coq_PArith_BinPosDef_Pos_compare()(
    |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:383:4
    |
383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::O...
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
509 |           self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
    |                                                ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
   --> src/main.rs:509:11
    |
509 |             self.Coq_PArith_BinPosDef_Pos_compare()(
    |             -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
    |  ___________|
    | |
510 | |             v)(
    | |______________- call expression requires function

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
   --> src/main.rs:784:14
    |
784 |   match self.Coq_PArith_BinPosDef_Pos_compare()(
    |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
    |
note: method defined here
   --> src/main.rs:383:4
    |
383 | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::O...
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
    |
784 |   match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
    |                                              ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
   --> src/main.rs:784:9
    |
784 |     match self.Coq_PArith_BinPosDef_Pos_compare()(
    |           -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
    |  _________|
    | |
785 | |           self.CertiCoq_Benchmarks_lib_vs_clause_prio(
786 | |             cl1))(
    | |_________________- call expression requires function

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
    --> src/main.rs:2689:18
     |
2689 |       match self.Coq_PArith_BinPosDef_Pos_compare()(
     |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
     |
note: method defined here
    --> src/main.rs:383:4
     |
383  | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::...
     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
     |
2689 |       match self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
     |                                                  ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
    --> src/main.rs:2689:13
     |
2689 |         match self.Coq_PArith_BinPosDef_Pos_compare()(
     |               -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
     |  _____________|
     | |
2690 | |               i)(
     | |________________- call expression requires function

error[E0308]: mismatched types
    --> src/main.rs:3765:29
     |
3762 |                             self.CertiCoq_Benchmarks_lib_vs_mergeC(
     |                                  --------------------------------- arguments to this method are incorrect
...
3765 | /                             self.Coq_Init_Datatypes_id()(
3766 | |                               ()),
     | |_________________________________^ expected `&dyn Fn(&...) -> ...`, found `&dyn Fn(())`
     |
     = note: expected reference `&dyn Fn(&CertiCoq_Benchmarks_lib_vs_expr<'_>) -> &CertiCoq_Benchmarks_lib_vs_expr<'_>`
                found reference `&dyn Fn(())`
note: method defined here
    --> src/main.rs:3658:4
     |
3658 | fn CertiCoq_Benchmarks_lib_vs_mergeC<A: Copy, B: Copy>(&'a self, A_cmp: &'a dyn Fn(A) -> &'a dyn Fn(A) -> std::cmp::Ordering, B_cmp: &'a dyn Fn(B) -> &'a dyn Fn(B) -> std::cmp::Ordering, fAB: &'a dyn Fn(A) -> B, a...
     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^                                                                                                                                                       -----------------------

error[E0061]: this method takes 2 arguments but 0 arguments were supplied
    --> src/main.rs:6533:10
     |
6533 |     self.Coq_PArith_BinPosDef_Pos_compare()(
     |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- two arguments of type `u64` and `u64` are missing
     |
note: method defined here
    --> src/main.rs:383:4
     |
383  | fn Coq_PArith_BinPosDef_Pos_compare(&'a self, a: u64, b: u64) -> std::cmp::...
     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^           ------  ------
help: provide the arguments
     |
6533 |     self.Coq_PArith_BinPosDef_Pos_compare(/* u64 */, /* u64 */)(
     |                                          ~~~~~~~~~~~~~~~~~~~~~~

error[E0618]: expected function, found `std::cmp::Ordering`
    --> src/main.rs:6533:5
     |
6533 |       self.Coq_PArith_BinPosDef_Pos_compare()(
     |       -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^- help: consider using a semicolon here to finish the statement: `;`
     |  _____|
     | |
6534 | |       i)(
     | |________- call expression requires function

Some errors have detailed explanations: E0061, E0308, E0618.
For more information about an error, try `rustc --explain E0061`.
error: could not compile `vs_hard` (bin "vs_hard") due to 13 previous errors

Sha fast

   Compiling sha_fast v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/certicoqwasm-rustextraction/benchmarks/rust/sha_fast-extracted)
error[E0282]: type annotations needed
   --> src/main.rs:620:24
    |
67  |                 let $p2 = n.unsigned_abs();
    |                           - type must be known at this point
...
620 |     self.closure(move |x0| {
    |                        ^^
    |
help: consider giving this closure parameter an explicit type
    |
620 |     self.closure(move |x0: /* Type */| {
    |                          ++++++++++++

For more information about this error, try `rustc --explain E0282`.
error: could not compile `sha_fast` (bin "sha_fast") due to 1 previous error

The text was updated successfully, but these errors were encountered:

workingjubilee · 2024-03-19T00:33:07Z

minor comment:

Sha fast: It is not guaranteed that type inference will succeed or that the inference algorithm will remain unchanged. If the types are known to the code generator, the generated code should emit the type annotations at appropriate binding sites, like closure arguments. Even if this was not done in every place possible (and it should probably only be done in a few places), this would make the code more resilient to small changes in the inference algorithm.

spitters · 2024-03-19T11:18:25Z

Thanks @womeier !
Quick answer. It looks like the Coq code uses loop as a term, which is a keyword in rust.
I believe there is some renaming going on in the rust extraction to catch this, but apparently not for "loop".
One could either rename loop to loop42 in the extraction, or write an algorithm that makes sure one generates a fresh name.

spitters · 2024-03-19T11:24:21Z

Welcome @workingjubilee ! Thanks for your interest in the experimental (!) rust extraction. Have you tried it yourself on examples?

There is some type information available at extraction time, but it may not be complete. See sec 5.5 here https://arxiv.org/pdf/2108.02995.pdf

4ever2 · 2024-03-19T15:41:05Z

@spitters I believe that this exact issue with renaming the loop keyword was discussed before (cannot remember where) but I don't think we have any pre-processing step to rename keywords.

We definitely need some better tests for the rust extraction plugin.

The remaining issues with vs_easy and vs_hard looks to be related to remapping of the stdlib type positive.

workingjubilee · 2024-03-19T16:46:39Z

I believe there is some renaming going on in the rust extraction to catch this, but apparently not for "loop".

Prefixing some of these idents with r# should work, allowing the following code to compile:

fn main() {
    let r#loop = loop {
        
    };
}

This may be a more general solution.

workingjubilee · 2024-03-19T18:05:06Z

Welcome @workingjubilee ! Thanks for your interest in the experimental (!) rust extraction. Have you tried it yourself on examples?

Honestly, you have won my attention by managing to induce SIGSEGV in the Rust compiler! I will try to make the binom.v Rust extraction compile, but I recommend avoiding that pattern in the future.

There is some type information available at extraction time, but it may not be complete.

For some cases, partial type information can be annotated via turbofished type arguments with an underscore to indicate the absent part, where relevant, e.g.

let v = iter.collect::<Vec<_>>();

spitters · 2024-03-20T19:40:22Z

@womeier For rust extraction we have the following tests:
Ack and even:
https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/InternalFix.v
W:
https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/BernsteinYangTermination.v

I think they should be relevant as general benchmarks for certicoq.

womeier · 2024-03-21T16:11:02Z

@womeier For rust extraction we have the following tests: Ack and even: https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/InternalFix.v W: https://github.com/AU-COBRA/coq-rust-extraction/blob/master/tests/theories/BernsteinYangTermination.v

I think they should be relevant as general benchmarks for certicoq.

yes, we'll include them. thanks!

womeier · 2024-04-03T22:23:38Z

Quick update: we needed a few more small manual fixes

some i64 annotations when using ExtrRustUncheckedArith
removing the derive(Debug) at a few places
reduced the error for vs_easy: replaced loop with loop42, and extracted without the remapping of nats (this introduced the additional problems in the original error in the issue description)
(some more information on our general setup here)

vs easy

 error[E0308]: mismatched types
    --> src/main.rs:4243:29
     |
4240 |                             self.CertiCoq_Benchmarks_lib_vs_mergeC(
     |                                  --------------------------------- arguments to this method are incorrect
...
4243 | /                             self.Coq_Init_Datatypes_id()(
4244 | |                               ()),
     | |_________________________________^ expected `&dyn Fn(&...) -> ...`, found `&dyn Fn(())`
     |
     = note: expected reference `&dyn Fn(&CertiCoq_Benchmarks_lib_vs_expr<'_>) -> &CertiCoq_Benchmarks_lib_vs_expr<'_>`
                found reference `&dyn Fn(())`
note: method defined here
    --> src/main.rs:4136:4
     |
4136 | fn CertiCoq_Benchmarks_lib_vs_mergeC<A: Copy, B: Copy>(&'a self, A_cmp: &'a dyn Fn(A) -> &'a dyn Fn(A) -> &'a Coq_Init_Datatypes_comparison<'a>, B_cmp: &'a dyn Fn(B) -> &'a dyn Fn(B) -> &'a Coq_Init_Datatypes_comparison<'a>, fAB: &'a dyn Fn(A) -> B, a...
     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^                                                                                                                                                                                             -----------------------

For more information about this error, try `rustc --explain E0308`.
error: could not compile `vs_easy` (lib) due to 1 previous error
</p>
</details>

womeier changed the title ~~Generated code doesn't compile~~ Generated rust code doesn't compile Mar 18, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Generated rust code doesn't compile #16

Generated rust code doesn't compile #16

womeier commented Mar 18, 2024 •

edited

Loading

workingjubilee commented Mar 19, 2024 •

edited

Loading

spitters commented Mar 19, 2024

spitters commented Mar 19, 2024

4ever2 commented Mar 19, 2024

workingjubilee commented Mar 19, 2024

workingjubilee commented Mar 19, 2024

spitters commented Mar 20, 2024

womeier commented Mar 21, 2024

womeier commented Apr 3, 2024 •

edited

Loading

Generated rust code doesn't compile #16

Generated rust code doesn't compile #16

Comments

womeier commented Mar 18, 2024 • edited Loading

What works

What doesn't work (see compilation errors below)

Rust extraction setup in one diff

To set up yourself

Versions

Errors

workingjubilee commented Mar 19, 2024 • edited Loading

spitters commented Mar 19, 2024

spitters commented Mar 19, 2024

4ever2 commented Mar 19, 2024

workingjubilee commented Mar 19, 2024

workingjubilee commented Mar 19, 2024

spitters commented Mar 20, 2024

womeier commented Mar 21, 2024

womeier commented Apr 3, 2024 • edited Loading

womeier commented Mar 18, 2024 •

edited

Loading

workingjubilee commented Mar 19, 2024 •

edited

Loading

womeier commented Apr 3, 2024 •

edited

Loading