01mf02 / kontroli-rs Goto Github PK

Hello!

What happened

I wrote the following term in some file

impi: (A: Prop) -> (B: Prop) -> Prf A -> Prf B

and kontroli scolded me saying Error: Parse(Term(AbstWithoutRhs)). Since I've been initiated to the ways of the logical frameworks, I could decipher AbstWithoutRhs, but no abstraction were involved. Even more confused, I asked Dedukti what it thought of that term, and it was happy with it. Reading again the error, I figured out it must be that there's a syntactic construction supported by Dedukti but not Kontroli, but which one? The readme gives examples of Dedukti files, and a "Differences with Dedukti" section, but the example files don't say what's not supported, and the difference section doesn't talk about the syntax. I then tried my luck and removed the parens on the products, et voila.

The issues, or what I'd have expected

The potential problems I see there are, in increasing order of time needed to fix it

• I couldn't find the subset of the syntax that is supported
• The error message is partly misleading
• Kontroli doesn't support the syntax (x: A) -> B

I could provide some documentation, but I'm not sure I could do anything for the two more complicated options.

Environment

• kocheck 0.4.1

Hi Michael. I tested kontroli on the translation of the HOL-Light base library to Dedukti (http://files.inria.fr/blanqui/hol-for-kocheck.dk.gz) and it seems slower than dkcheck.
Using a computer with 32 processors Intel(R) Core(TM) i9-13950HX with 36Mo cache and 64Go RAM.
dk check runs in 4m11s.
kocheck -j32 runs in 5m33s (and doesn't seem to use all the processors at full speed).

Hello,
the commands

git clone https://github.com/01mf02/kontroli-rs
cd kontroli-rs
cargo run -p kocheck --release examples/pure.dk

fail with the following message

[...]
Compiling spinning_top v0.2.4
error[E0658]: use of unstable library feature 'renamed_spin_loop'
  --> <home/directory>/.cargo/registry/src/github.com-1ecc6299db9ec823/spinning_top-0.2.4/src/spinlock.rs:57:17
   |
57 |                 hint::spin_loop();
   |                 ^^^^^^^^^^^^^^^
   |
   = note: for more information, see https://github.com/rust-lang/rust/issues/55002

error: aborting due to previous error

For more information about this error, try `rustc --explain E0658`.
error: could not compile `spinning_top`.
warning: build failed, waiting for other jobs to finish...
error: build failed

With rust version

$ rustc --version
rustc 1.41.1

(on Debian buster, btw, it has been updated 👍)

The following commmands

git clone https://github.com/01mf02/kontroli-rs
cd kontroli-rs
cargo run -p kocheck --release examples/pure.ko

produce the unexpected following output

error[E0658]: use of unstable library feature 'mem_take'
    --> /home/u/.cargo/registry/src/github.com-1ecc6299db9ec823/im-14.3.0/./src/vector/mod.rs:1160:33
     |
1160 |                         middle: std::mem::take(&mut tree.middle),
     |                                 ^^^^^^^^^^^^^^
     |
     = note: for more information, see https://github.com/rust-lang/rust/issues/61129

error[E0658]: use of unstable library feature 'mem_take'
    --> /home/u/.cargo/registry/src/github.com-1ecc6299db9ec823/im-14.3.0/./src/vector/mod.rs:1181:33
     |
1181 |                         middle: std::mem::take(&mut tree.middle),
     |                                 ^^^^^^^^^^^^^^
     |
     = note: for more information, see https://github.com/rust-lang/rust/issues/61129

error: aborting due to 2 previous errors

For more information about this error, try `rustc --explain E0658`.
error: Could not compile `im`.
warning: build failed, waiting for other jobs to finish...
error: build failed

I use rustc 1.38.0

Hi Michael. Would it be possible to accept the keywords "#REQUIRE" and "injective", even if you do nothing with them? This would help using kocheck with currently produced dk files without having to modify them beforehand.