Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Hi @makarius, hi @adelon,
I have recently adopted the current Naproche master branch for the new webinterface at https://naproche.github.io/
For this I have made the following changes:
network
package. Unfortunately, this means that it is necessary to split Naproche into three different packages:app
,Isabelle
andsrc
. The parts of the Isabelle sources that do not usenetwork
are now found undersrc/Isabelle
, while those that usenetwork
are underIsabelle
. Last year, I was able to keep theIsabelle
sources together in mydev
branch by creating anIsabelle
package that shared its sources with thenaproche
package. But this is not possible here, as the sources now describe common types likeBytes
and GHC would get confused ifBytes
from theIsabelle
package is the same thing asBytes
from the Naproche package.MonadFile
,MessageExchangeContext
andRunProverContext
that abstract from these system calls. There is aConsole
context with a basic implementation insrc/
itself and aPIDE
context inapp/
(which depends onIsabelle/
).ImportQualifiedPost
extension and adding aMonadFail
instance in the parser.