Re: [isabelle-dev] Complete Distributive Lattice

[Viorel Preoteasa]

My changes to Complete Distributive Lattices are now integrated in the
development version of Isabelle.

I want to thank Manuel Eberl for helping with testing and pushing the
update into repository.

Viorel Preoteasa

On Fri, Mar 9, 2018 at 12:48 PM, Lawrence Paulson <l...@cam.ac.uk> wrote:

> I don’t think it’s a problem that your more general theorems require the
> Axiom of Choice, and Hilbert_Choice.thy is not too large already (far from
> it).
>
> Larry Paulson
>
>
>
> > On 8 Mar 2018, at 21:35, <viorel.preote...@gmail.com> <
> viorel.preote...@gmail.com> wrote:
> >
> > I have a question about how to organize these changes. The problem is
> that most of the results for the more general lattice (instantiations
> > to set, fun) require Hilbert_Choice which is not available in
> Complete_Lattice. Now I have added all results about complete distributive
> > lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this
> acceptable?
> >
>
>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Viorel Preoteasa]

I have been very busy, but I will find time to work on it.

Viorel


On 11/23/2017 6:46 PM, Lawrence Paulson wrote:
Whatever happened with this? The new release has been out for a while, 
and it would make sense to integrate your work now, well before any 
thought of a new release.

Larry

On 27 Aug 2017, at 15:59, Viorel Preoteasa <viorel.preote...@aalto.fi 
<mailto:viorel.preote...@aalto.fi>> wrote:


I managed to integrate the new complete distributive lattice into HOL 
library.


The changes are these:

Complete_Lattice.thy
- replaced the complete_distrib_lattice with the new stronger version.
- moved some proofs about complete_distrib_lattice and some 
instantiations to Hilbert_Choice


Hilbert_Choice.thy
- added all results complete_distrib_lattice, including instantiations
of set, fun that uses uses Hilbert choice.

Enum.thy
- new proofs that finite_3 and finite_4 are complete_distrib_lattice.
- I added here the classes finite_lattice and finite_distrib_lattice
and proved that they are complete. This simplified quite much the proofs
that finite_3 and finite_4 are complete_distrib_lattice.

Predicate.thy
- new proof that predicates are complete_distrib_lattice.

I compiled HOL in Isabelle2017-RC0 using

isabelle build -v -c HOL

and I got:

Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 
43.344s GC time, factor 1.83)

Finished HOL (0:04:26 elapsed time)

Finished at Sun Aug 27 17:41:30 GMT+3 2017
0:04:37 elapsed time

But I don't now how to go from here to have these changes into Isabelle.

There is also AFP. If there are instantiations of 
complete_distrib_lattice, then most probably they will fail.


One simple solution in this case could be to keep also the
old complete_distrib_lattice as complete_pseudo_distrib_lattice.

Viorel


On 8/26/2017 3:06 PM, Lawrence Paulson wrote:
On 25 Aug 2017, at 20:14, Viorel Preoteasa 
<viorel.preote...@aalto.fi <mailto:viorel.preote...@aalto.fi> 
<mailto:viorel.preote...@aalto.fi>> wrote:


One possible solution:

Add the new class in Complete_Lattice.thy, replacing the existing class

Prove the instantiations and the complete_linearord subclass later
in Hilbert_Choice.

On the other hand, it seems inconvenient to have the Hilbert Choice
to depend on so many other theories.

I’d prefer this provided the instantiations aren’t needed earlier.
The delay in the introduction of the Axiom of Choice is partly 
historical, but it’s worth noting how much of HOL can be developed 
without it.

Larry




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

Re: [isabelle-dev] Complete Distributive Lattice

[Viorel Preoteasa]

OK, I understand, what is the time frame for going back to normal? I did 
spent some time on this and I would like to see it finished.


As I mentioned earlier, I added finite lattices to simplify the proofs
in Enum.thy that finite_n are distributive complete lattices. However,
searching for dependencies on complete_distrib_lattice, I found a very 
similar class of finite lattices in Library. How should this be handled?


Viorel

On 8/28/2017 5:26 PM, Lawrence Paulson wrote:
For sure. The work is very welcome, but too drastic to undertake at this 
precise moment.

Larry

On 28 Aug 2017, at 13:08, Makarius > wrote:


Nothing of this is relevant for the Isabelle2017 release. When the "RC"
versions show up, it is time to finish and not to start new things.



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

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Viorel Preoteasa]

On 8/27/2017 6:11 PM, Lawrence Paulson wrote:

In the AFP, grep picks up these:

~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r .
./Coinductive/Examples/CCPO_Topology.thy
./Concurrent_Ref_Alg/Refinement_Lattice.thy
./DataRefinementIBP/Diagram.thy
./DataRefinementIBP/Hoare.thy
./DataRefinementIBP/Statements.thy
./LatticeProperties/Conj_Disj.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy
./PSemigroupsConvolution/Quantales.thy

But why would they fail? The new version is surely stronger, so any 
changes should be pretty straightforward, right?




They will fail only if there are instantiations of the new class, since 
it is stronger. I will check these files. I discovered some files also

src/HOL/Library that need to be updated.

Some of the AFP files from this list are from my submissions.

Viorel


Larry

On 27 Aug 2017, at 15:59, Viorel Preoteasa <viorel.preote...@aalto.fi 
<mailto:viorel.preote...@aalto.fi>> wrote:


There is also AFP. If there are instantiations of 
complete_distrib_lattice, then most probably they will fail.


One simple solution in this case could be to keep also the
old complete_distrib_lattice as complete_pseudo_distrib_lattice.




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

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Viorel Preoteasa]

I managed to integrate the new complete distributive lattice into HOL 
library.


The changes are these:

Complete_Lattice.thy
 - replaced the complete_distrib_lattice with the new stronger version.
 - moved some proofs about complete_distrib_lattice and some 
instantiations to Hilbert_Choice


Hilbert_Choice.thy
 - added all results complete_distrib_lattice, including instantiations
of set, fun that uses uses Hilbert choice.

Enum.thy
 - new proofs that finite_3 and finite_4 are complete_distrib_lattice.
 - I added here the classes finite_lattice and finite_distrib_lattice
and proved that they are complete. This simplified quite much the proofs
that finite_3 and finite_4 are complete_distrib_lattice.

Predicate.thy
 - new proof that predicates are complete_distrib_lattice.

I compiled HOL in Isabelle2017-RC0 using

isabelle build -v -c HOL

and I got:

Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 43.344s 
GC time, factor 1.83)

Finished HOL (0:04:26 elapsed time)

Finished at Sun Aug 27 17:41:30 GMT+3 2017
0:04:37 elapsed time

But I don't now how to go from here to have these changes into Isabelle.

There is also AFP. If there are instantiations of 
complete_distrib_lattice, then most probably they will fail.


One simple solution in this case could be to keep also the
old complete_distrib_lattice as complete_pseudo_distrib_lattice.

Viorel


On 8/26/2017 3:06 PM, Lawrence Paulson wrote:
On 25 Aug 2017, at 20:14, Viorel Preoteasa <viorel.preote...@aalto.fi 
<mailto:viorel.preote...@aalto.fi>> wrote:


One possible solution:

Add the new class in Complete_Lattice.thy, replacing the existing class

Prove the instantiations and the complete_linearord subclass later
in Hilbert_Choice.

On the other hand, it seems inconvenient to have the Hilbert Choice
to depend on so many other theories.


I’d prefer this provided the instantiations aren’t needed earlier.

The delay in the introduction of the Axiom of Choice is partly 
historical, but it’s worth noting how much of HOL can be developed 
without it.


Larry

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

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Viorel Preoteasa]

I have investigated the possibility of replacing the existing 
complete_distrib_lattice with the stronger version.


Here are the problems:

1. The new class needs Hilbert choice in few places: proving the dual
of the distributivity property, proving the set and fun instantiations,
and proving that complete_linearord is subclass of the new class. I
think that the Hilbert choice cannot be avoided, as for example
Wikipedia page states that no nontrivial instance of this could exists
without the axiom of choice.

2. Hilbert_Choice comes very late in the library, and depends on the
Complete_Lattice.thy

One possible solution:

Add the new class in Complete_Lattice.thy, replacing the existing class

Prove the instantiations and the complete_linearord subclass later
in Hilbert_Choice.

Another possibility is to move everything related to complete
distributive lattice in a new theory that imports Hilbert_Choice,
but I don't know if the current distributivity properties are used
before Hilbert_Choice.

On the other hand, it seems inconvenient to have the Hilbert Choice
to depend on so many other theories.

Viorel

On 8/24/2017 6:40 PM, Florian Haftmann wrote:

As far as I remember, I introduced the complete_distrib_lattice class
after realizing the a complete lattice whose binary operations are
distributive is not necessarily a distributive complete lattice.  Hence
the specification of that type class has been contrieved without
consulting literature.

Hence that change should be fine if someone is willing to undertake it
before the RC stabilization phase.

Cheers,
Florian

Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:

Sounds good to me. Can anybody think of an objection?
Larry


On 23 Aug 2017, at 15:17, Viorel Preoteasa <viorel.preote...@aalto.fi
<mailto:viorel.preote...@aalto.fi>> wrote:

Hello,

I am not sure if this is the right place to post this message, but it is
related to  the upcoming release as I am prosing adding something
to the Isabelle library.

While working with complete distributive lattices, I noticed that
the Isabelle class complete_distrib_lattice is weaker compared to
what it seems to be regarded as a complete distributive lattice.

As I needed the more general concept, I have developed it,
and if Isabelle community finds it useful to be in the library,
then I could provide the proofs or integrate it myself in the
Complete_Lattice.thy

The only axiom needed for complete distributive lattices is:

Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈
Y)})"

and from this, the equality and its dual can be proved, as well as
the existing axioms of complete_distrib_lattice and the instantiation
to bool, set and fun.

Best regards,

Viorel


On 2017-08-21 21:24, Makarius wrote:

Dear Isabelle contributors,

we are now definitely heading towards the Isabelle2017 release.

The first official release candidate Isabelle2017-RC1 is anticipated for
2/3-Sep-2017, that is a bit less than 2 weeks from now.

That is also the deadline for any significant additions.


I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
in Isabelle/5c0a3f63057d, but it seems that many potential entries are
still missing.

Please provide entries in NEWS and CONTRIBUTORS for all relevant things
you have done since the last release.


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


___
isabelle-dev mailing list
isabelle-...@in.tum.de <mailto: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




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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Viorel Preoteasa]

On 2017-08-24 23:25, Manuel Eberl wrote:

Purely out of interest: Does this also hold for filters?

Manuel


Do filters form a complete lattice? It seems that a filter of a lattice 
should be nonempty.
I think that this condition would prevent the set of filters to be a 
lattice.


If empty set is accepted as a filter, then one could have a complete lattice
of filters (filter will be closed to arbitrary intersections). But I 
don't know

if this complete lattice is distributive.

Viorel



On 2017-08-24 20:54, Viorel Preoteasa wrote:

I have now a file with the new class, and all necessary proofs
(both distributivity equalities, bool, set, fun interpretations,
proofs of the old distributivity properties).

I have also the proof that complete linear order is subclass of
the new complete distributive lattice class.

Are there any other subclasses of the current complete distributive
lattice class? This would be something that could cause problems.

Otherwise, the existing complete distrib lattice is subclass
of the one that I implemented, so it should not cause any problems.
All existing results in the current class can be reused without
modification.

My theory works now in Isabelle 2016-1, but I can try it in
Isabelle2017-RC0 also.

I can try to integrate it, but I don't know how to test it
to see if there are any problems with something else.

For reference, I attach the theory file with the new
class of complete distributive lattice.

Best regards,

Viorel



On 8/24/2017 6:40 PM, Florian Haftmann wrote:

As far as I remember, I introduced the complete_distrib_lattice class
after realizing the a complete lattice whose binary operations are
distributive is not necessarily a distributive complete lattice.  Hence
the specification of that type class has been contrieved without
consulting literature.

Hence that change should be fine if someone is willing to undertake it
before the RC stabilization phase.

Cheers,
 Florian

Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:

Sounds good to me. Can anybody think of an objection?
Larry


On 23 Aug 2017, at 15:17, Viorel Preoteasa <viorel.preote...@aalto.fi
<mailto:viorel.preote...@aalto.fi>> wrote:

Hello,

I am not sure if this is the right place to post this message, but
it is
related to  the upcoming release as I am prosing adding something
to the Isabelle library.

While working with complete distributive lattices, I noticed that
the Isabelle class complete_distrib_lattice is weaker compared to
what it seems to be regarded as a complete distributive lattice.

As I needed the more general concept, I have developed it,
and if Isabelle community finds it useful to be in the library,
then I could provide the proofs or integrate it myself in the
Complete_Lattice.thy

The only axiom needed for complete distributive lattices is:

Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈
Y)})"

and from this, the equality and its dual can be proved, as well as
the existing axioms of complete_distrib_lattice and the instantiation
to bool, set and fun.

Best regards,

Viorel


On 2017-08-21 21:24, Makarius wrote:

Dear Isabelle contributors,

we are now definitely heading towards the Isabelle2017 release.

The first official release candidate Isabelle2017-RC1 is
anticipated for
2/3-Sep-2017, that is a bit less than 2 weeks from now.

That is also the deadline for any significant additions.


I have already updated the important files NEWS, CONTRIBUTORS,
ANNOUNCE
in Isabelle/5c0a3f63057d, but it seems that many potential entries are
still missing.

Please provide entries in NEWS and CONTRIBUTORS for all relevant
things
you have done since the last release.


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


___
isabelle-dev mailing list
isabelle-...@in.tum.de <mailto: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




___
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


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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Viorel Preoteasa]

Hello,

I am not sure if this is the right place to post this message, but it is
related to  the upcoming release as I am prosing adding something
to the Isabelle library.

While working with complete distributive lattices, I noticed that
the Isabelle class complete_distrib_lattice is weaker compared to
what it seems to be regarded as a complete distributive lattice.

As I needed the more general concept, I have developed it,
and if Isabelle community finds it useful to be in the library,
then I could provide the proofs or integrate it myself in the
Complete_Lattice.thy

The only axiom needed for complete distributive lattices is:

Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})"

and from this, the equality and its dual can be proved, as well as
the existing axioms of complete_distrib_lattice and the instantiation
to bool, set and fun.

Best regards,

Viorel


On 2017-08-21 21:24, Makarius wrote:

Dear Isabelle contributors,

we are now definitely heading towards the Isabelle2017 release.

The first official release candidate Isabelle2017-RC1 is anticipated for
2/3-Sep-2017, that is a bit less than 2 weeks from now.

That is also the deadline for any significant additions.


I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
in Isabelle/5c0a3f63057d, but it seems that many potential entries are
still missing.

Please provide entries in NEWS and CONTRIBUTORS for all relevant things
you have done since the last release.


Makarius
___
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] Isabelle/jEdit build

[Viorel Preoteasa]

Hi,

I managed to get it working with the latest version of jedit_build.
However, I could only get it using scala-2.8.2.final and not with
scala-2.9.1-1.

Using scala-2.9.1-1 on OS X Lion generates the error:

### Building Isabelle/jEdit ...
4:18:55 PM [main] [error] PluginJAR: Error while starting plugin 
isabelle.jedit.Plugin
4:18:55 PM [main] [error] PluginJAR: java.lang.NoClassDefFoundError: 
scala/Serializable
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass1(Native Method)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClassCond(ClassLoader.java:631)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass(ClassLoader.java:615)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass(ClassLoader.java:465)
4:18:55 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:439)
4:18:55 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:109)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:247)
4:18:55 PM [main] [error] PluginJAR:  at 
isabelle.jedit.Plugin.init(plugin.scala:385)
4:18:55 PM [main] [error] PluginJAR:  at 
sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
4:18:55 PM [main] [error] PluginJAR:  at 
sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:39)
4:18:55 PM [main] [error] PluginJAR:  at 
sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:27)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.reflect.Constructor.newInstance(Constructor.java:513)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.Class.newInstance0(Class.java:355)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.Class.newInstance(Class.java:308)
4:18:55 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:735)
4:18:55 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:823)
4:18:55 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.jEdit.main(jEdit.java:486)
4:18:55 PM [main] [error] PluginJAR: Caused by: 
java.lang.ClassNotFoundException: scala.Serializable
4:18:55 PM [main] [error] PluginJAR:  at 
java.net.URLClassLoader$1.run(URLClassLoader.java:202)
4:18:55 PM [main] [error] PluginJAR:  at 
java.security.AccessController.doPrivileged(Native Method)
4:18:55 PM [main] [error] PluginJAR:  at 
java.net.URLClassLoader.findClass(URLClassLoader.java:190)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:306)
4:18:55 PM [main] [error] PluginJAR:  at 
sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:301)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:247)
4:18:55 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader.loadFromParent(JARClassLoader.java:522)
4:18:55 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:87)
4:18:55 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:247)

4:18:55 PM [main] [error] PluginJAR:  ... 17 more
4:18:55 PM [main] [error] ErrorListDialog$ErrorEntry: 
/Users/viorel/Work/isabelle-dev/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
4:18:55 PM [main] [error] ErrorListDialog$ErrorEntry: Cannot start: 
java.lang.NoClassDefFoundError: scala/Serializable
4:18:55 PM [main] [error] ErrorListDialog$ErrorEntry: Try updating to a 
newer version of the plugin.

lemon:isabelle viorel$ bin/isabelle jedit
4:21:20 PM [main] [error] PluginJAR: Error while starting plugin 
isabelle.jedit.Plugin
4:21:20 PM [main] [error] PluginJAR: java.lang.NoClassDefFoundError: 
scala/Serializable
4:21:20 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass1(Native Method)
4:21:20 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClassCond(ClassLoader.java:631)
4:21:20 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass(ClassLoader.java:615)
4:21:20 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass(ClassLoader.java:465)
4:21:20 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:439)
4:21:20 PM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:109)
4:21:20 PM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:247)
4:21:20 PM [main] [error] PluginJAR:  at 
isabelle.jedit.Plugin.init(plugin.scala:385)
4:21:20 PM [main] [error] PluginJAR:  at 
sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
4:21:20 PM [main] [error] PluginJAR:  at 
sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:39)
4:21:20 PM [main] [error] PluginJAR:  at 

[isabelle-dev] compiling jedit for Isabelle development

[Viorel Preoteasa]

Hello,

I am trying to use jedit with the Isabelle development version

I have scala-2.9.1-1 and I downloaded jedit_build-20120313.

I set the paths

export 
SCALA_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib/scala-2.9.1-1
export 
ISABELLE_JEDIT_BUILD_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib/jedit_build-20120313


in bin/isabelle

When I start isabelle with jedit, I get the errors:

### Building Isabelle/jEdit ...
cp: dist/properties/.: No such file or directory
cp: dist/modes/.: No such file or directory
cp: src/modes/.: unable to copy extended attributes to dist/modes/.: No 
such file or directory

cp: dist/modes/./isabelle-session.xml: No such file or directory
cp: dist/modes/./isabelle.xml: No such file or directory
cp: dist/modes/./scala.xml: No such file or directory
cp: utimes: dist/modes/.: No such file or directory
cp: chown: dist/modes/.: No such file or directory
cp: chmod: dist/modes/.: No such file or directory
cp: chflags: dist/modes/.: No such file or directory
cp: src/modes/.: unable to copy ACL to dist/modes/.: No such file or 
directory

Can't open dist/modes/catalog: No such file or directory at -e line 1.
usage: cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file target_file
   cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file ... 
target_directory


I notices that there is also the directory 
/Users/viorel/Work/isabelle-dev/isabelle/src/Tools/jEdit/


which contains what jedit_build-20120313 contains plus additional things.
However setting

export 
ISABELLE_JEDIT_BUILD_HOME=/Users/viorel/Work/isabelle-dev/isabelle/src/Tools/jEdit


it fails with

### Building Isabelle/jEdit ...
cp: /Users/viorel/Work/isabelle-dev/isabelle/src/Tools/jEdit/contrib//.: 
No such file or directory

cp: dist/properties/.: No such file or directory
cp: dist/modes/.: No such file or directory
cp: src/modes/.: unable to copy extended attributes to dist/modes/.: No 
such file or directory

cp: dist/modes/./isabelle-session.xml: No such file or directory
cp: dist/modes/./isabelle.xml: No such file or directory
cp: dist/modes/./scala.xml: No such file or directory
cp: utimes: dist/modes/.: No such file or directory
cp: chown: dist/modes/.: No such file or directory
cp: chmod: dist/modes/.: No such file or directory
cp: chflags: dist/modes/.: No such file or directory
cp: src/modes/.: unable to copy ACL to dist/modes/.: No such file or 
directory

Can't open dist/modes/catalog: No such file or directory at -e line 1.
usage: cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file target_file
   cp [-R [-H | -L | -P]] [-fi | -n] [-apvX] source_file ... 
target_directory

Failed!

The file src/Tools/jEdit/README_BUILD says  to set ISABELLE_JEDIT_BUILD_HOME
via init_component .../jedit_build..., but I don't know how to do it.

Best regards,

Viorel

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

Re: [isabelle-dev] compiling jedit for Isabelle development

[Viorel Preoteasa]

On 3/27/12 11:59 PM, Makarius wrote:

On Tue, 27 Mar 2012, Viorel Preoteasa wrote:


I am trying to use jedit with the Isabelle development version

I have scala-2.9.1-1 and I downloaded jedit_build-20120313.

I set the paths

export 
SCALA_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib/scala-2.9.1-1
export 
ISABELLE_JEDIT_BUILD_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib/jedit_build-20120313


The file src/Tools/jEdit/README_BUILD says  to set 
ISABELLE_JEDIT_BUILD_HOME

via init_component .../jedit_build..., but I don't know how to do it.


Isabelle settings are configured via etc/settings, either directly 
e.g. in your ~/.isabelle/etc/settings (for repository versions) or by 
initializing some Isabelle component.  The Isabelle System manual 
explains the general principles behind etc/settings and etc/components.


The jedit_build-20120313 directory is already such a component, so if 
you say init_component .../jedit_build-20120313 in your settings it 
should work.
I managed to get this setting working. I have used the file 
../isabelle/etc/settings.
I was afraid that using the local .isabelle will overwrite the settings 
for the

release version of Isabelle (Isabelle2011-1).

After setting init_component .../jedit_build-20120313 I managed to 
compile jedit,
however I run into another problem. When starting isabelle jedit, I get 
an error

that some class is not found.

I am using OS X Lion (10.7.3). Both JAVA_HOME and ISABELLE_JDK_HOME are 
set to:


/System/Library/Java/JavaVirtualMachines/1.6.0.jdk/Contents/Home

using the script:
export JAVA_HOME=$(/usr/libexec/java_home -v 1.6)
export ISABELLE_JDK_HOME=$(/usr/libexec/java_home -v 1.6)

The error I get is:

12:04:21 AM [main] [error] PluginJAR: Error while starting plugin 
isabelle.jedit.Plugin
12:04:21 AM [main] [error] PluginJAR: java.lang.NoClassDefFoundError: 
scala/Serializable
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass1(Native Method)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClassCond(ClassLoader.java:631)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass(ClassLoader.java:615)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.defineClass(ClassLoader.java:465)
12:04:21 AM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:439)
12:04:21 AM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:109)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:247)
12:04:21 AM [main] [error] PluginJAR:  at 
isabelle.jedit.Plugin.init(plugin.scala:385)
12:04:21 AM [main] [error] PluginJAR:  at 
sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
12:04:21 AM [main] [error] PluginJAR:  at 
sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:39)
12:04:21 AM [main] [error] PluginJAR:  at 
sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:27)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.reflect.Constructor.newInstance(Constructor.java:513)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.Class.newInstance0(Class.java:355)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.Class.newInstance(Class.java:308)
12:04:21 AM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:735)
12:04:21 AM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:823)
12:04:21 AM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.jEdit.main(jEdit.java:486)
12:04:21 AM [main] [error] PluginJAR: Caused by: 
java.lang.ClassNotFoundException: scala.Serializable
12:04:21 AM [main] [error] PluginJAR:  at 
java.net.URLClassLoader$1.run(URLClassLoader.java:202)
12:04:21 AM [main] [error] PluginJAR:  at 
java.security.AccessController.doPrivileged(Native Method)
12:04:21 AM [main] [error] PluginJAR:  at 
java.net.URLClassLoader.findClass(URLClassLoader.java:190)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:306)
12:04:21 AM [main] [error] PluginJAR:  at 
sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:301)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:247)
12:04:21 AM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader.loadFromParent(JARClassLoader.java:522)
12:04:21 AM [main] [error] PluginJAR:  at 
org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:87)
12:04:21 AM [main] [error] PluginJAR:  at 
java.lang.ClassLoader.loadClass(ClassLoader.java:247)

12:04:21 AM [main] [error] PluginJAR:  ... 17 more
12:04:21 AM [main] [error] ErrorListDialog$ErrorEntry: 
/Users/viorel/Work/isabelle-dev/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
12:04:21 AM [main] [error] ErrorListDialog$ErrorEntry: Cannot start: 
java.lang.NoClassDefFoundError