Kind1

Kind1 copied to clipboard

Compiler doesn't support erasing functions

1

Here's a reproductible sample if we want to support erasing functions or just warn the user that he's trying to use, at runtime, a variable that is erased (here `size`...

elmattic

Compiler is not checking usage of erased arguments

1

Here is a minimal code sample to reproduce the error: ``` foo(dummy: Word(size)): Word(size) Word.zero(size) Main: IO(Unit) do IO { let x = 7 let w = Word.from_bits(4, Nat.to_bits(x)) ::...

elmattic

I think it would be useful that formality exits with an error code if it can't typecheck something.

Eloitor

Accept multiple files on check command

1

Useful to check all files in a folder after adding many things or changing something that could break many other functions.

developedby

algebraic-dev

Some functions are present in the Kind2 genesis block thus they should not be compiled.

algebraic-dev

developedby

Sort kind names after loading all files

1

This prevents the HVM rules from being generated in different order every time. Refresh the checker.hvm file to be in the new sorted order

developedby

The command `cargo install kind2` return: ```bash Compiling unicode-normalization v0.1.21 error: failed to run custom build command for `openssl-sys v0.9.75` Caused by: process didn't exit successfully: `/tmp/cargo-installeokYEg/release/build/openssl-sys-51c18241c0871913/build-script-main` (exit status: 101)...

SergioBonatto

Does the compiler run on WebAssembly (wasm)? Is such feature planned?

flip111