Closed kensh closed 9 years ago
yes, because currently our large amount of syntax stretched the sdf2tbl tool too much, that the Mac and Cygwin version of this tool fails to generate tbl files. The Linux version of this tool is still working, so it is only kompilable on Linux.
thanks, laurayuwen
ok, I will try the older version of java-semantics, instead of the latest. Could you advice me which git version of java-semantics are runnable on Mac?
9840cfde929795e834397fb7f4ac98f87ee88c64 This one should be ok on Mac, it's just after I changed tools scripts to incorporate Mac
If the version suggested above does not work, I recommend you to try this one: https://github.com/kframework/java-semantics/tree/popl-artifact-evaluation
The instructions in /docs are guaranteed to work.
thanks laurayuwen, denis-bogdanas
I removed git depth and checkout your recommend-version of java-semantics 9840cfd following is working fine on my Mac Book Air Yosemite 10.10.2
Installation process for Mac:
$ cd ~ $ git clone https://github.com/kframework/java-semantics.git $ git checkout 9840cfde929795e834397fb7f4ac98f87ee88c64 $ chmod +x java-semantics/tools/* $ export PATH=$PATH:~/java-semantics/tools $ cd java-semantics/src $ kjkompile.sh
I tried to run kjkompile.sh on my Mac and got following IO error.
$ kjkompile.sh --debug
Preprocessing semantics: java.io.FileNotFoundException: Source 'prep/.k/kompile8699375838561766857/ground/Concrete.tbl' does not exist at org.apache.commons.io.FileUtils.copyFile(FileUtils.java:871) at org.apache.commons.io.FileUtils.copyFile(FileUtils.java:835) at org.kframework.parser.DefinitionLoader.parseDefinition(DefinitionLoader.java:224) at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:86) at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:181) at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:161) at org.kframework.kompile.KompileFrontEnd.main(KompileFrontEnd.java:72) at org.kframework.main.Main.main(Main.java:49) [Error] Internal: IO error detected writing ground parser to file
Execution semantics: java.io.FileNotFoundException: Source 'exec/.k/kompile1837892923315791969/ground/Concrete.tbl' does not exist at org.apache.commons.io.FileUtils.copyFile(FileUtils.java:871) at org.apache.commons.io.FileUtils.copyFile(FileUtils.java:835) at org.kframework.parser.DefinitionLoader.parseDefinition(DefinitionLoader.java:224) at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:86) at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:181) at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:161) at org.kframework.kompile.KompileFrontEnd.main(KompileFrontEnd.java:72) at org.kframework.main.Main.main(Main.java:49) [Error] Internal: IO error detected writing ground parser to file
Done
I checked the directories $ls java-semantics/src/exec/.k/kompile1837892923315791969/ground Common.sdf Integration.sdf KTechnique.sdf Concrete.sdf KBuiltinsBasic.sdf
$ls java-semantics/src/prep/.k/kompile8699375838561766857/ground Common.sdf Integration.sdf KTechnique.sdf Concrete.sdf KBuiltinsBasic.sdf
there are only .sdf files and no .tbl files
I used recommended version of kframework https://github.com/kframework/k/releases/tag/v3.4 java version "1.8.0_31"
Does anyone know the solution about this?