Re: [isabelle-dev] Repository version of Isabelle on Windows 7

[Anders Schlichtkrull]

On Fri, 30 Oct 2015, Makarius wrote:

> Somehow the downloaded csdp-6.x.tar.gz came out as corrupted.  Just delete 
> that file and try "isabelle components -a" again.

The file csdp-6.x.tar.gz was completely empty. I followed your suggestion and 
now the output showed that the different .tar.gz files were downloaded and 
unpacked. I therefore continued following README_REPOSITORY with the following 
result:

Anders@r099121 /cygdrive/c/repo-isabelle/isabelle
$ ./bin/isabelle jedit -l HOL
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 1.4
warning: [options] source value 1.4 is obsolete and will be removed in a future 
release
warning: [options] target value 1.4 is obsolete and will be removed in a future 
release
warning: [options] To suppress warnings about obsolete options, use 
-Xlint:-options.
Note: GraphBrowser\GraphBrowser.java uses or overrides a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
4 warnings
### Building Isabelle/Scala ...
Concurrent\simple_thread.scala:45: error: object getProperty is not a member of 
package System
  val m = 
Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) 
getOrElse 0
  ^
General\bytes.scala:32: error: object arraycopy is not a member of package 
System
  System.arraycopy(a, offset, b, 0, length)
 ^
General\bytes.scala:104: error: object arraycopy is not a member of package 
System
  System.arraycopy(bytes, offset, new_bytes, 0, length)
 ^
General\bytes.scala:105: error: object arraycopy is not a member of package 
System
  System.arraycopy(other.bytes, other.offset, new_bytes, length, 
other.length)
 ^
General\time.scala:19: error: object currentTimeMillis is not a member of 
package System
  def now(): Time = ms(System.currentTimeMillis())
  ^
System\platform.scala:18: error: object getProperty is not a member of package 
System
  val is_macos = System.getProperty("os.name", "") == "Mac OS X"
^
System\platform.scala:19: error: object getProperty is not a member of package 
System
  val is_windows = System.getProperty("os.name", "").startsWith("Windows")
  ^
System\platform.scala:37: error: object getProperty is not a member of package 
System
  System.getProperty("os.arch", "") match {
 ^
System\platform.scala:45: error: object getProperty is not a member of package 
System
  System.getProperty("os.name", "") match {
 ^
System\platform.scala:60: error: object getProperty is not a member of package 
System
System.getProperty("java.version") match {
   ^
System\platform.scala:68: error: object getProperty is not a member of package 
System
  val jvm_name: String = System.getProperty("java.vm.name", "")
^
GUI\gui.scala:33: error: object getProperty is not a member of package System
find_laf(System.getProperty("isabelle.laf")) getOrElse {
^
System\isabelle_system.scala:24: error: object getProperty is not a member of 
package System
val java_home = System.getProperty("java.home", "")
   ^
System\isabelle_system.scala:40: error: object getenv is not a member of 
package System
  check(System.getenv(envar)) orElse  // e.g. inherited from running 
isabelle tool
   ^
System\isabelle_system.scala:41: error: object getProperty is not a member of 
package System
  check(System.getProperty(property)) getOrElse  // e.g. via JVM 
application boot process
   ^
System\isabelle_system.scala:90: error: object getenv is not a member of 
package System
  val temp = if (Platform.is_windows) System.getenv("TEMP") else null
 ^
System\isabelle_system.scala:93: error: object getProperty is not a member of 
package System
val user_home = System.getProperty("user.home", "")
   ^
System\isabelle_system.scala:94: error: object getProperty is not a member of 
package System
val isabelle_app = System.getProperty("isabelle.app", "")
  ^
Tools\main.scala:68: error: object setProperty is not a member of package System
System.setProperty("jedit.home", 
File.platform_path(Path.explode("$JEDIT_HOME/dist")))
   ^
Tools\main.scala:69: error: object setProperty is not a member of package System
System.setProperty("scala.home", 
File.platform_path(Path.explode("$SCALA_HOME")))
   ^
Tools\main.scala:110: error: object getenv is not a member of package System
update(m.get(System.getenv()))
^
21 errors found
Failed to compile sources

Anders@r099121 /cygdrive/c/repo-isabelle/isabelle
$

Cheers and thanks,
Anders Schlichtkrull

Re: [isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

 On 09 November, 2015 11:56 CET, Makarius  wrote: 
 
> It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure 
> as separate command. If there is a simple way to have just one 
> 'interpretation' command with 'defines' vs. 'rewrites', I would prefer 
> that.

I would prefer to just have 'interpretation' as well.  Possibly 'sublocale' 
should also be extended by a 'defines' clause.

Clemens
 
 


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

[isabelle-dev] NEWS: State panel

[Makarius]

* The State panel manages explicit proof state output, with jEdit action
"isabelle.update-state" (shortcut S+ENTER) to trigger update according
to cursor position.

* The Output panel no longer shows proof state output by default. This
reduces resource requirements of prover time and GUI space.
INCOMPATIBILITY, use the State panel instead or enable option
"editor_output_state".


This refers to Isabelle/bb20f11dd842.  The State panel has been around for 
a while, without mentioning it explicitly.  It should now be sufficiently 
consolidated for production use; even old GUI timing problems that caused 
excessive flashing due to repaints should no longer happen.


Disabling option editor_output_state allows to get back to the traditional 
Isabelle/jEdit behaviour, but tradtionalists might actually like the new 
State panel better, because it is closer to Proof General (in the newer 
3-buffer model, not the truely traditional 2-buffer model).



Makarius

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

Re: [isabelle-dev] Future of permanent_interpretation

[Makarius]

What is the conclusion of this thread for the coming release? Whatever 
happens, the time window for it is approx. Nov/Dec 2015.


Historically, the 'permanent_interpretation' command had to stay outside 
Isabelle/Pure and Main Isabelle/HOL, because it was overwriting the 
'interpretation' command in an ad-hoc manner -- causing a lot of confusion 
to everybody.  (This incident also accelerated the strict discpline of 
authentic commands.)


It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure 
as separate command. If there is a simple way to have just one 
'interpretation' command with 'defines' vs. 'rewrites', I would prefer 
that.



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

Re: [isabelle-dev] Repository version of Isabelle on Windows 7

[Makarius]

On Mon, 9 Nov 2015, Anders Schlichtkrull wrote:


### Building Isabelle/Scala ...
Concurrent\simple_thread.scala:45: error: object getProperty is not a member of 
package System
 val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", 
"0")) getOrElse 0


Odd.  I've seen something like this many years ago, with rather old 
versions of Scala, but it did not happen recently.


What is the result of "isabelle getenv SCALA_HOME"?

To make double sure: can you delete ISABELLE_HOME/lib/classes/Pure.jar and 
try again?  Or try "isabelle jedit -bf".



In principle, this should all work routinely.  I am building from 
repository myself with Windows 2008, Windows 7, Windows 8.1, Windows 10.



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