K-user mailing list

[<daparpon AT dsic.upv.es>]

Hi! I am interested in trying out the verification features of K 4.0 (latest
distribution in GitHub), so I downloaded and installed it and checked that the
binaries work as expected. However, when I went to compile the KernelC
language specification provided for verification (in the samples/kernelc
folder), I found that there are dependencies that apparently are not included
in the distribution. More specifically, the following lines in samples/
kernelc/kernelc.k point to a file and a module that are nowhere to be found:

require "patterns/int_set.k"
imports VERIFICATION_LEMMAS

I tried to comment them and compile the language anyway (in case they were
deprecated dependencies), but kompile gives me the following error, indicating
that they are still needed:

[Error] Compiler: Had 46 parsing errors.
[Error] Critical: Could not infer a unique sort for variable 'IntSet'.
Possible
sorts: Bag@KCELLS, List@LIST, Set@SET, Map@MAP
        Source(/Users/elp/Documents/k/samples/kernelc/./patterns/int_list.k)
        Location(33,8,33,45)
[Error] Critical: Could not infer a unique sort for variable 'IntSet'.
Possible
sorts: Id@ID, Set@SET, VariableDeclarations@KERNELC-SYNTAX,
Globals@KERNELC-SYNTAX, Map@MAP, Statements@KERNELC-SYNTAX, Bag@KCELLS,
List@LIST
        Source(/Users/elp/Documents/k/samples/kernelc/./patterns/
tree_pattern.k)
        Location(15,8,15,34)
[Error] Inner Parser: Parse error: unexpected character ')'.
        Source(/Users/elp/Documents/k/samples/kernelc/./kernelc-semantics.k)
        Location(287,52,287,53)
... (more similar errors referring to IntSet occurrences)

How can I solve this problem? I have been trying to get the verification
infrastructure of K to work for a long, long time, and I keep continuously
running into issues about it...

Thanks in advance,
Daniel