Re: [isabelle-dev] NEWS: Isabelle/VSCode

[Simon Wimmer]

Hi Makarius,

the same goes for me. Installing and running this worked without any
trouble when following your instructions.
One thing that disturbed me in the beginning was that I first have to edit
a document before any symbols get prettified.

Simon

On Mon, Jul 3, 2017 at 4:11 PM Mathias Fleury 
wrote:

> Dear Makarius,
>
> I am using Isabelle/VSCode code for a week now. So it is possible to
> install and use it.
>
>
> I mostly like it:
>
>- I really like VSCode's Control-P to search for commands.
>
>- the PIDE protocol, unlike "isabelle build", accepts unicode
>characters: If the file contains "×⇩r" instead of "\\<^sub>r" (e.g.
>because I copy-pasted it) , Isabelle/jEdit and Isabelle/VSCode will accept
>the expression, but "isabelle build" will fail. It took a long time to
>figure that out, since in Iaabelle/jEdit, the symbols are shown in the same
>fashion.
>
>- there are some weird slow-downs: Every once in a while,
>refreshing/jumping to the definition take several seconds. I am not yet
>sure whether Isabelle or VSCode is responsible.
>
>
> Mathias
>
>
>
> On 01.07.17 19:36, Makarius wrote:
>
> *** General ***
>
> * Experimental support for Visual Studio Code (VSCode) as alternative
> Isabelle/PIDE front-end, see 
> alsohttps://marketplace.visualstudio.com/items?itemName=makarius.isabelle
>
> VSCode is a new type of application that continues the concepts of
> "programmer's editor" and "integrated development environment" towards
> fully semantic editing and debugging -- in a relatively light-weight
> manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
> Technically, VSCode is based on the Electron application framework
> (Node.js + Chromium browser + V8), which is implemented in JavaScript
> and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
> modules around a Language Server implementation.
>
>
> This refers to Isabelle/8f39d60b943d. The marketplace link above also
> shows a screenshot.
>
> I am interested to hear if anybody manages to run the application:
> presently it lacks the all-inclusive application bundling of Isabelle/jEdit.
>
>
>   Makarius
> ___
> isabelle-dev mailing 
> listisabelle-...@in.tum.dehttps://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Uses of Jenkins at TUM

[Simon Wimmer]

Hi Makarius,

I think everyone involved with this issue is interested in coming back to a
situation where we have a solution that works for everyone.
Can we try to find a proposal for a change of the current infrastructure
that accommodates for yours and others' missing requirements?

On Mon, Apr 24, 2017 at 6:12 PM Makarius  wrote:

> On 24/04/17 14:46, Makarius wrote:
> >
> > Are there users of it outside the TUM group?
> >
> > What is good about it? What is bad about it?
>
> (1) To follow the line of Mira vs. Jenkins:
>
>   * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.


>   * I did not find this information in Jenkins, when I was still
> spending more time on it last year.


Is what Dmitriy pointed out (the status page) sufficient?


>   * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.
>

We can think of multiple solutions to bring down the testboard build times
to 'quasi-interactive'.
This could also include incremental builds for the distribution if wanted.
Would you use the testboard if this was possible?


> (2) To follow the line of Jenkins vs. isatest:
>
> When Jenkins was about to supersede isatest last year, I put forward
> missing requirements e.g. here:
>
> http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg06783.html


Let me restate these:

* Realistic tests with typical settings. This means that x86 (and not
x86_64) is used by default. We've recently seen mysterious resource
problems occasionally, and the automatic testing infrastructure should be
able to point quickly to relevant changesets.

We now have a periodic build job for x86, too. Why would you still opt for
x86 as a default, considering it is very hard to get rid of spurious
failures in this setting (as Lars pointed out below)?

* Decent performance measurements and charts: both multi-core run-time and
heap space requirements.

Your point of criticism seems to be that the currently available charts are
not as reliable as what was available many years ago. However, this seems
to already have been a problem in the pre-Jenkins times. Can you suggest a
scheme to get more reliable measurements?


>
>
> Today we have already the isatest sucessor "isabelle_cronjob" in
> Isabelle/Scala, and a proper discussion wrt. Jenkins needs to continue
> there. See also
>
> http://isabelle.in.tum.de/repos/isabelle/file/f8681c62959d/src/Pure/Admin/isabelle_cronjob.scala
>
> The latter is all about Isabelle administration infrastructure, i.e. the
> parts that are only seen when they don't work properly.
>
>
What I take away from this thread so far is that most users generally seem
to be happy with the Jenkins infrastructure. Thus, we are happy to continue
the discussion, but I do not see why we would need a completely different
testing infrastructure.


>
> Makarius
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Simon
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev