Cannot compile

[t4sk]

Hi
First of all thanks for creating this!

I've tried compiling erc20.k but it fails with the following message:

[Error] Compiler: Could not find sorts: [Bool]
	Source(/mount/erc20.k)
	Location(16,19,16,22)

Any help would be much appreciated. Thanks

Detail

Installed k-framework using docker

Created a container, copied erc20.k and ran

k-distribution/target/release/k/bin/kompile /mount/erc20.k 

Log

root@21880d35cb6b:/k# k-distribution/target/release/k/bin/kompile /mount/erc20.k 

WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$2 (file:/k/k-distribution/target/release/k/lib/java/guice-4.0-beta5.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$2
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
[Error] Compiler: Could not find sorts: [Bool]
	Source(/mount/erc20.k)
	Location(16,19,16,22)

[suhabe]

I'm also getting this error:

$ kompile imp.k
[Error] Compiler: Could not find sorts: [Bool]
Source(~/erc20-semantics/erc20.k)
Location(16,19,16,22)

$ kompile --version
RV-K version 1.0-SNAPSHOT
Git revision: b577155
Git branch: master
Build date: Mon Feb 11 16:39:22 PST 2019

[tomtomjhj]

@suhabe Looks like it uses the previous version of k. I think it would be better to check out ERC777 semantic which subsumes ERC20 and uses recent K.

[tomtomjhj]

@suhabe Oh, actually there is a branch using current K.

[suhabe]

Thank you!

The k5 branch worked, except that I had to change the tests/imp/Makefile by replacing KOMPILE_FLAGS=--backend java with KOMPILE_BACKEND?=java. Otherwise, I would get the following error:

$ cd ~/erc20-semantics/tests/imp
$ make
~/k/k-distribution/bin/kompile --backend java --backend ocaml  imp.k -d .
[Error] Critical: Can only specify option --backend once. (Can only specify
option --backend once.)

Created a PR for this edit: #3

[chenIshi]

After checking out to k5 branch and kompile imp.k, it still have some syntax error

File "realdef.ml", line 3654, characters 304-305:
Error: Syntax error: ')' expected
File "realdef.ml", line 3654, characters 280-281:
Error: This '(' might be unmatched
[Error] Critical: ocamlopt returned nonzero exit code: 2
Examine output to see errors.
[Warning] Compiler: Could not find main syntax module with name IMP-SYNTAX in
definition. Use --syntax-module to specify one. Using IMP as default.
[Warning] Compiler: missing entry for hook BAG.concat
[Warning] Compiler: missing entry for hook BAG.element
[Warning] Compiler: missing entry for hook BAG.unit

After config the makefile variable $K_HOME, and call make again, this problem is solved.

[charlotte-Zch]

@chenIshi how should i config the $K_HOME?