On Thu, 25 Jun 2015, Ramana Kumar wrote:
> Everyone is welcome!
>
> A draft program can be found on the workshop website:
> https://www.cl.cam.ac.uk/~rk436/hol15/
Thanks for welcoming even non-HOL4 guys like myself. As can be seen on
the program, I've got a rather generous slot with hacking and discussion
about the following topic:
Isabelle/PIDE/jEdit as integrated development environment for Standard ML
After more than 7 years of development, Isabelle/PIDE/jEdit is today the
standard way to interact with that particular proof assistant. In
Isabelle2015 (May 2015) the TTY-based REPL and its wrapper for Proof
General / Emacs have already been dismantled. This radical move might be
taken as an opportunity of the HOL4 community to attract former Isabelle
users who really do want to use plain TTY interaction. Or as an
opportunity to discuss possibilities for HOL4 users and developers to
make their own moves towards full-scale IDE support.
As a very modest start, I would like to present various possibilities of
Isabelle/PIDE to operate as IDE for Standard ML, which happens to be the
underlying language platform of HOL4 as well. This touches various
facilities of Poly/ML that David Matthews provides specifically to tool
builders: run-time compiler invocation with IDE feedback, toplevel
environment management, structured toplevel printing (with markup and
hyperlinks), and potentially also run-time debugging of SML (still
unused in Isabelle2015).
Beyond that it is also possible to integrate any other languages that
are related or unrelated to the prover platform, using PIDE libraries
either on the ML or Scala side of that IDE framework.
If anybody has specific interests, it is possible to tell me beforehand
(privately or here on the list) so that I can adjust the workshop
presentation accordingly.
Makarius
------------------------------------------------------------------------------
Monitor 25 network devices or servers for free with OpManager!
OpManager is web-based network management software that monitors
network devices and physical & virtual servers, alerts via email & sms
for fault. Monitor 25 devices for free with no restriction. Download now
http://ad.doubleclick.net/ddm/clk/292181274;119417398;o
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
