search

kframework / kweb

Online extensible IDE for the K Framework and other formal verification projects. Example deployment at http://kframework.org/kweb/
5 stars 5 forks source link

Kcompile does not work when user is logged in #11

Closed vlad-doru closed 10 years ago

vlad-doru commented 10 years ago

Running command: kompile bf.k java.io.FileNotFoundException: /srv/kweb/kfiles/default/samples/bf/bf-kompiled/def/Concrete.sdf (No such file or directory) at java.io.FileOutputStream.open(Native Method) at java.io.FileOutputStream.(Unknown Source) at java.io.FileOutputStream.(Unknown Source) at org.kframework.parser.utils.ResourceExtractor.Extract(ResourceExtractor.java:10) at org.kframework.parser.utils.ResourceExtractor.ExtractDefSDF(ResourceExtractor.java:24) at org.kframework.parser.DefinitionLoader.parseDefinition(DefinitionLoader.java:147) at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:81) at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:289) at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:262) at org.kframework.main.Main.main(Main.java:49) java.io.FileNotFoundException: /srv/kweb/kfiles/default/samples/bf/bf-kompiled/defx-maude.bin (No such file or directory) at java.io.FileOutputStream.open(Native Method) at java.io.FileOutputStream.(Unknown Source) at java.io.FileOutputStream.(Unknown Source) at org.kframework.utils.BinaryLoader.save(BinaryLoader.java:11) at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:83) at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:289) at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:262) at org.kframework.main.Main.main(Main.java:49) java.lang.NullPointerException at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:290) at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:262) at org.kframework.main.Main.main(Main.java:49) java.io.FileNotFoundException: /srv/kweb/kfiles/default/samples/bf/bf-kompiled/compile-options.bin (No such file or directory) at java.io.FileOutputStream.open(Native Method) at java.io.FileOutputStream.(Unknown Source) at java.io.FileOutputStream.(Unknown Source) at org.kframework.utils.BinaryLoader.save(BinaryLoader.java:11) at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:263) at org.kframework.main.Main.main(Main.java:49) ----- End of process output.

pdaian commented 10 years ago

Fixed in the newest kweb for all new users.

If you are still having this issue, a solution would be to modify any file in the collection that's giving an error (just type anything and wait for it to say saved). Then, refresh the page and all should be working again.

Thanks for reporting, feel free to comment again if you feel the issue hasn't been resolved :).