martinring / cobra Goto Github PK
View Code? Open in Web Editor NEWProof and Code Presentation Framework
Home Page: http://www.flatmap.net/cobra/
License: GNU Lesser General Public License v3.0
Proof and Code Presentation Framework
Home Page: http://www.flatmap.net/cobra/
License: GNU Lesser General Public License v3.0
Using global /tmp files without any precautions is a bit fragile. What happens when more than one instance of Cobra is running on the same machine, even by different users?
Moreover, just with one instance, I ran into a situation where /tmp/Haskell.hs contained some old garbage that was not shown in the presentation. Consequently, ghc-mod
produced errors that were unclear, like
Info: Multiple declarations of ‘f’
Declared at: /tmp/Haskell.hs:7:1
/tmp/Haskell.hs:10:1
These multple occurrences for f where just old junk.
Note that Isabelle/Scala uses java.nio.file.Files.createTempFile
for the implementation of Isabelle_System.tmp_file.
Now, this may not be easy to trace as I haven't found a way to reproduce this yet, but after having my Cobra instance running for some time, it seems to get stuck in some kind of loop, which leads to the presentation website being refreshed every second und thus becoming unusable.
I've had this happen to me several times already. The console is spammed with a repeating error message:
[ERROR] [10/04/2016 13:18:54.530] [01_Einleitung-akka.actor.default-dispatcher-398] [akka.actor.ActorSystemImpl(01_Einleitung)] WebSocket handler failed with Cannot subscribe to shut-down Publisher (akka.stream.impl.ActorPublisher$NormalShutdownException)
Are there any logs that may be helpful for hunting this down?
Scala presentation compiler can only be accessed on designated thread. This crash is easily reproducible for me if I select a name in any nontrivial piece of code.
____ _
/ ___|___ | |__ _ __ __ _ TM
| | / _ \| '_ \| '__/ _` |
| |__| (_) | |_) | | | (_| |
\____\___/|_.__/|_| \__,_|
________________________________________
| version 1.0.5 - (c) 2016 Martin Ring |
[INFO] [06/23/2016 10:37:09.033] [scratch-akka.actor.default-dispatcher-3] [scratch] serving presentation from /Users/psp/scratch/cobra-scratch/scratch
[INFO] [06/23/2016 10:37:09.034] [scratch-akka.actor.default-dispatcher-3] [scratch] server is listening on localhost:8080
[INFO] [06/23/2016 10:37:10.300] [scratch-akka.actor.default-dispatcher-8] [scratch] initializing new scala document 'code_snippet_1'
[ERROR] [06/23/2016 10:37:15.677] [scratch-akka.actor.default-dispatcher-14] [akka.actor.LocalActorRefProvider(akka://scratch)] guardian failed, shutting down system
java.lang.AssertionError: assertion failed: Race condition detected: You are running a presentation compiler method outside the PC thread.[phase: <no phase>] Please file a ticket with the current stack trace at https://www.assembla.com/spaces/scala-ide/support/tickets
at scala.tools.nsc.interactive.Global.assertCorrectThread(Global.scala:537)
at scala.reflect.internal.Symbols$Symbol.rawInfo(Symbols.scala:1590)
at scala.reflect.internal.Symbols$Symbol.signatureString(Symbols.scala:2676)
at scala.reflect.internal.Symbols$Symbol.defString(Symbols.scala:2724)
at scala.reflect.internal.TypeDebugging$$anonfun$typeParamsString$1.apply(TypeDebugging.scala:149)
at scala.reflect.internal.TypeDebugging$$anonfun$typeParamsString$1.apply(TypeDebugging.scala:149)```
Starting a second instance of cobra does not use the next available port or at least handles the error nicely but instead shows an exception stacktrace on the console and seems to just crash the application:
$ cobra
____ _
/ ___|___ | |__ _ __ __ _ TM
| | / _ \| '_ \| '__/ _` |
| |__| (_) | |_) | | | (_| |
\____\___/|_.__/|_| \__,_|
________________________________________
| version 1.0.5 - (c) 2016 Martin Ring |
[ERROR] [10/10/2016 12:18:44.350] [01_Einleitung-akka.actor.default-dispatcher-2] [akka://01_Einleitung/system/IO-TCP/selectors/$a/0] Bind failed for TCP channel on endpoint [localhost/127.0.0.1:8080]
java.net.BindException: Die Adresse wird bereits verwendet
at sun.nio.ch.Net.bind0(Native Method)
at sun.nio.ch.Net.bind(Net.java:433)
at sun.nio.ch.Net.bind(Net.java:425)
at sun.nio.ch.ServerSocketChannelImpl.bind(ServerSocketChannelImpl.java:223)
at sun.nio.ch.ServerSocketAdaptor.bind(ServerSocketAdaptor.java:74)
at akka.io.TcpListener.liftedTree1$1(TcpListener.scala:55)
at akka.io.TcpListener.<init>(TcpListener.scala:52)
at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
at java.lang.reflect.Constructor.newInstance(Constructor.java:423)
at akka.util.Reflect$.instantiate(Reflect.scala:65)
at akka.actor.ArgsReflectConstructor.produce(IndirectActorProducer.scala:96)
at akka.actor.Props.newActor(Props.scala:213)
at akka.actor.ActorCell.newActor(ActorCell.scala:562)
at akka.actor.ActorCell.create(ActorCell.scala:588)
at akka.actor.ActorCell.invokeAll$1(ActorCell.scala:461)
at akka.actor.ActorCell.systemInvoke(ActorCell.scala:483)
at akka.dispatch.Mailbox.processAllSystemMessages(Mailbox.scala:282)
at akka.dispatch.Mailbox.run(Mailbox.scala:223)
at akka.dispatch.Mailbox.exec(Mailbox.scala:234)
at scala.concurrent.forkjoin.ForkJoinTask.doExec(ForkJoinTask.java:260)
at scala.concurrent.forkjoin.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1339)
at scala.concurrent.forkjoin.ForkJoinPool.runWorker(ForkJoinPool.java:1979)
at scala.concurrent.forkjoin.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:107)
[ERROR] [10/10/2016 12:18:44.351] [01_Einleitung-akka.actor.default-dispatcher-5] [01_Einleitung] binding failed with bind failed
Typing "?" into a code box (e.g. Haskell) inserts that into the text and pops up the presentation help screen.
The theory node of code class="isabelle" is something like code_snippet_1.thy, which means the content needs to start with "theory code_snippet_1 imports Main begin". This is both inconvenient and looks very odd in a presentation.
currently we are relying on a custom websocket adapter for client server communication. integrating akka.js would allow for greater flexibility.
Should be ~/.config/cobra.conf on linux
~/Library/Preferences/cobra.conf on macOS
and ~/AppData/.../cobra.conf on windows
With a slides.html containing
<section>
<code src="como.scala"></code>
</section>
Where como.scala contains the code sample from #18, both safari and chrome render it like this:
I am not sure what is up with the huge whitespace margin at the top and left, but it would be great to reclaim it. It's also anywhere from difficult to impossible to view and modify the code which doesn't fit on screen. There's no scrollbar; mouse scroll doesn't work; selecting into the text and dragging past the end of the window does move us downward while I pull, but as soon as I let go - or when I reach the end of the file - it bounces back up to only display the initial lines.
Trying to work with Isabelle/ML, I've produced an external file like this:
theory Test_ML
imports Main
begin
ML ‹
(** begin #isabelle-ml *)
(** end #isabelle-ml *)
›
end
This does not quite work: the system prints some undefined
things and produces non-sense.
Admittedly, this approach stretches the meta-comment feature a bit far.
should be moved from dfki-theme to isabelle.less
Snippet management on the client is far from optimal and brings numerous issues. It should be moved to the server.
Secure mode for isabelle_process (option -S) does not make much sense: as a local application the user is expected to know what he is doing. Also note that this option has been discontinued in the repository version after Isabelle2016 -- it is not really secure, but may mislead people to think they get a secure system.
Without secure mode in Isabelle2016, it is e.g. possible to use the ML command to demonstrate Isabelle/ML.
Enable Executable / Evaluatable Snippets
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.