K Framework is not compatible with c-semantics master (fails even with Docker and bundled submodule) #660
Description
Hi team,
I’ve been trying to build and run the c-semantics repository using the master branch, both natively (on Ubuntu 18.04 via WSL) and inside Docker, but the process consistently fails due to incompatibilities with the K Framework — even the one bundled as a submodule.
Here are the key issues encountered:
org.kframework.utils.errorsystem.KEMException: [Error] Compiler: Could not find module: K-EQUAL-SYNTAX$SYNTAX at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:126) at org.kframework.utils.errorsystem.KEMException.compilerError(KEMException.java:72) at org.kframework.definition.FlatModule.resolveImport$1(outer-ext.scala:96) at org.kframework.definition.FlatModule.$anonfun$toModule$4(outer-ext.scala:99) at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234) at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320) at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976) at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976) at scala.collection.TraversableLike.map(TraversableLike.scala:234) at scala.collection.TraversableLike.map$(TraversableLike.scala:227) at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47) at scala.collection.SetLike.map(SetLike.scala:101) at scala.collection.SetLike.map$(SetLike.scala:101) at scala.collection.AbstractSet.map(Set.scala:47) at org.kframework.definition.FlatModule.toModule(outer-ext.scala:99) at org.kframework.kore.convertors.KILtoKORE.apply(KILtoKORE.java:109) at org.kframework.parser.concrete2kore.ParserUtils.lambda$loadModules$4(ParserUtils.java:223) at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:195) at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1654) at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:484) at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:474) at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:913) at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234) at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:578) at org.kframework.parser.concrete2kore.ParserUtils.loadModules(ParserUtils.java:223) at org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:275) at org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:256) at org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:187) at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:156) at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:165) at org.kframework.kompile.Kompile.run(Kompile.java:133) at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70) at org.kframework.main.FrontEnd.main(FrontEnd.java:62) at org.kframework.main.Main.runApplication(Main.java:118) at org.kframework.main.Main.runApplication(Main.java:108) at org.kframework.main.Main.main(Main.java:56) [Warning] Critical: The OCaml backend is in the process of being deprecated (final date May 31, 2020). Please switch to the LLVM backend. Makefile:56: recipe for target '/home/user/mounted/dist/profiles/x86-gcc-limited-libc/c-translation-kompiled/c-translation-kompiled/timestamp' failed make[1]: *** [/home/user/mounted/dist/profiles/x86-gcc-limited-libc/c-translation-kompiled/c-translation-kompiled/timestamp] Error 113 make[1]: Leaving directory '/home/user/mounted/semantics' Makefile:413: recipe for target 'c-translation-semantics' failed
org.kframework.utils.errorsystem.KEMException: [Error] Compiler: Had 2 parsing errors. at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:126) at org.kframework.utils.errorsystem.KEMException.compilerError(KEMException.java:72) at org.kframework.kompile.DefinitionParsing.throwExceptionIfThereAreErrors(DefinitionParsing.java:182) at org.kframework.kompile.DefinitionParsing.saveCachesAndReportParsingErrors(DefinitionParsing.java:146) at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:175) at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:165) at org.kframework.kompile.Kompile.run(Kompile.java:133) at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70) at org.kframework.main.FrontEnd.main(FrontEnd.java:62) at org.kframework.main.Main.runApplication(Main.java:118) at org.kframework.main.Main.runApplication(Main.java:108) at org.kframework.main.Main.main(Main.java:56) [Error] Inner Parser: Parse error: unexpected token 'End'. Source(/home/user/mounted/semantics/common/compat.k) Location(360,116,360,119) [Error] Inner Parser: Parse error: unexpected token 'Start'. Source(/home/user/mounted/semantics/common/compat.k) Location(363,55,363,60) [Warning] Critical: The OCaml backend is in the process of being deprecated (final date May 31, 2020). Please switch to the LLVM backend. Makefile:66: recipe for target '/home/user/mounted/dist/profiles/x86-gcc-limited-libc/c-cpp-linking-kompiled/c-cpp-linking-kompiled/timestamp' failed make[1]: *** [/home/user/mounted/dist/profiles/x86-gcc-limited-libc/c-cpp-linking-kompiled/c-cpp-linking-kompiled/timestamp] Error 113 make[1]: Leaving directory '/home/user/mounted/semantics' Makefile:413: recipe for target 'c-cpp-linking-semantics' failed make: *** [c-cpp-linking-semantics] Error 2
Work Arounds Tried So Far:
- Used make, make -j4, and make c-translation-semantics — all fail at different stages.
- Built K using the bundled .build/k submodule (git submodule update --init --recursive)
- Attempted Docker-based builds — same issues persisted.
- Tried manually patching the code (e.g., removing K-EQUAL-SYNTAX import), which just revealed more breakages.
Can you please:
Clarify which version (or commit) of K is currently known to be compatible with c-semantics master?