martinring / cobra Goto Github PK

View Code? Open in Web Editor NEW

21.0 21.0 3.0 329.36 MB

Proof and Code Presentation Framework

Home Page: http://www.flatmap.net/cobra/

License: GNU Lesser General Public License v3.0

Scala 86.91% HTML 1.49% CSS 10.40% Haskell 0.10% Isabelle 0.50% Shell 0.59%

cobra's People

Contributors

Stargazers

Watchers

Forkers

aruee nifni nilsmahlstaedt

cobra's Issues

Fragile /tmp files

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.

RPM/DNF breaks cobra path when updating

Support slides.md as alternative to slides.html

Memory leak: Obsolete Isabelle sessions are not terminated on reload

Cobra Crashes (Rebinding to closed Stream)

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

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)```

Custom Hover Annotations

Port being already in use is not handled well

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

Conflict of "?" in <code> vs. presentation

Typing "?" into a code box (e.g. Haskell) inserts that into the text and pops up the presentation help screen.

Automatically Install ghc-mod when not available locally

Use one prover instance per presentation (not per snippet)

code class="isabelle" expects generated theory name

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.

ISABELLE_HOME doesn't get picked up

switch to akka.js for the client

currently we are relying on a custom websocket adapter for client server communication. integrating akka.js would allow for greater flexibility.

Scala Syntax Highlighting is broken

Global Config

Should be ~/.config/cobra.conf on linux
~/Library/Preferences/cobra.conf on macOS
and ~/AppData/.../cobra.conf on windows

rendering issue

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.

Isabelle/ML snippet syntax problem

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.

MatchError: ENTRY_DELETE

Standard themes don't render certain token types in isabelle

should be moved from dfki-theme to isabelle.less

Automatically Download Isabelle when not available locally

Select token under cursor on hover

Move Snippet management to server.

Snippet management on the client is far from optimal and brings numerous issues. It should be moved to the server.

Pointless secure mode

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.