[isabelle] Isabelle repository won't build in an encrypted directory



Hi,

Firstly, does Isabelle have a bug tracker? If so, please direct me to it
and I'll post this there.

When cloning the Isabelle bitbucket repo and attempting to use it as per
README_REPOSITORY, it doesn't work if your working directory is in an
encrypted mount. I get the attached results. Somewhere in the mess of
error output is "File name too long." I've seen this issue before with
another tool that was generating temporary files in my (encrypted) home
directory. The standard Ubuntu home encryption setup stores per-file
metadata in your home directory in a path derived by extending the name
of the original file. If the original filename is quite long, extending
it will exceed the limits of the underlying file system. I believe
that's what is happening here.

Is it possible to resolve this issue in the repository?

OS: Ubuntu 12.04
uname -r: 3.2.0-35-generic
hg id: c633700b2d9f

Thanks,
Matt

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
$ hg clone https://bitbucket.org/makarius/isabelle
destination directory: isabelle
requesting all changes
adding changesets
adding manifests
adding file changes
added 50993 changesets with 131780 changes to 9165 files
updating to branch default
2913 files updated, 0 files merged, 0 files removed, 0 files unresolved
$ cd isabelle
$ ./bin/isabelle components -I
Initializing "/home/matthew/.isabelle/etc/settings"
$ ./bin/isabelle components -a
$ ./bin/isabelle jedit -l HOL
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 1.4
Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
1 warning
### Building Isabelle/Scala ...
error: 
     while compiling: term_xml.scala
        during phase: jvm
     library version: version 2.10.0
    compiler version: version 2.10.0
  reconstructed args: -target:jvm-1.5 -nowarn -d classes

  last tree to typer: Literal(Constant(Tuple2))
              symbol: null
   symbol definition: null
                 tpe: Class(classOf[scala.Tuple2])
       symbol owners: 
      context owners: object Term_XML$Decode -> package isabelle

== Enclosing template or block ==

Template( // val <local Decode>: <notype> in object Term_XML$Decode, tree.tpe=isabelle.Term_XML$Decode.type
  "java.lang.Object" // parents
  ValDef(
    private
    "_"
    <tpt>
    <empty>
  )
  // 5 statements
  ValDef( // private[this] val sort: Function1 in object Term_XML$Decode
    private <local> <triedcooking>
    "sort "
    <tpt> // tree.tpe=Function1
    <empty>
  )
  DefDef( // val sort(): Function1 in object Term_XML$Decode
    <method> <stable> <accessor> <triedcooking>
    "sort"
    []
    List(Nil)
    <tpt> // tree.tpe=Function1
    Term_XML$Decode.this."sort " // private[this] val sort: Function1 in object Term_XML$Decode, tree.tpe=Function1
  )
  DefDef( // def typ(): Function1 in object Term_XML$Decode
    <method> <triedcooking>
    "typ"
    []
    List(Nil)
    <tpt> // tree.tpe=Function1
    Apply( // def variant(fs: List): Function1 in object XML$Decode, tree.tpe=Function1
      "isabelle"."XML$Decode"."variant" // def variant(fs: List): Function1 in object XML$Decode, tree.tpe=(fs: List)Function1
      Apply( // override def apply(xs: Seq): List in object List, tree.tpe=List
        immutable.this."List"."apply" // override def apply(xs: Seq): List in object List, tree.tpe=(xs: Seq)List
        Apply( // implicit def wrapRefArray(xs: Array[Object]): collection.mutable.WrappedArray in class LowPriorityImplicits, tree.tpe=collection.mutable.WrappedArray
          scala.this."Predef"."wrapRefArray" // implicit def wrapRefArray(xs: Array[Object]): collection.mutable.WrappedArray in class LowPriorityImplicits, tree.tpe=(xs: Array[Object])collection.mutable.WrappedArray
          Apply( // final def $asInstanceOf[T0 >: ? <: ?](): T0 in class Object, tree.tpe=Array[Object]
            TypeApply( // final def $asInstanceOf[T0 >: ? <: ?](): T0 in class Object, tree.tpe=()Array[Object]
              Array[Function2]{{
  (new anonymous class anonfun$typ$4(): Function2)
}, {
  (new anonymous class anonfun$typ$5(): Function2)
}, {
  (new anonymous class anonfun$typ$6(): Function2)
}}."$asInstanceOf" // final def $asInstanceOf[T0 >: ? <: ?](): T0 in class Object, tree.tpe=[T0 >: ? <: ?]()T0
              <tpt> // tree.tpe=Array[Object]
            )
            Nil
          )
        )
      )
    )
  )
  DefDef( // def term(): Function1 in object Term_XML$Decode
    <method> <triedcooking>
    "term"
    []
    List(Nil)
    <tpt> // tree.tpe=Function1
    Apply( // def variant(fs: List): Function1 in object XML$Decode, tree.tpe=Function1
      "isabelle"."XML$Decode"."variant" // def variant(fs: List): Function1 in object XML$Decode, tree.tpe=(fs: List)Function1
      Apply( // override def apply(xs: Seq): List in object List, tree.tpe=List
        immutable.this."List"."apply" // override def apply(xs: Seq): List in object List, tree.tpe=(xs: Seq)List
        Apply( // implicit def wrapRefArray(xs: Array[Object]): collection.mutable.WrappedArray in class LowPriorityImplicits, tree.tpe=collection.mutable.WrappedArray
          scala.this."Predef"."wrapRefArray" // implicit def wrapRefArray(xs: Array[Object]): collection.mutable.WrappedArray in class LowPriorityImplicits, tree.tpe=(xs: Array[Object])collection.mutable.WrappedArray
          Apply( // final def $asInstanceOf[T0 >: ? <: ?](): T0 in class Object, tree.tpe=Array[Object]
            TypeApply( // final def $asInstanceOf[T0 >: ? <: ?](): T0 in class Object, tree.tpe=()Array[Object]
              Array[Function2]{{
  (new anonymous class anonfun$term$7(): Function2)
}, {
  (new anonymous class anonfun$term$8(): Function2)
}, {
  (new anonymous class anonfun$term$9(): Function2)
}, {
  (new anonymous class anonfun$term$10(): Function2)
}, {
  (new anonymous class anonfun$term$11(): Function2)
}, {
  (new anonymous class anonfun$term$12(): Function2)
}}."$asInstanceOf" // final def $asInstanceOf[T0 >: ? <: ?](): T0 in class Object, tree.tpe=[T0 >: ? <: ?]()T0
              <tpt> // tree.tpe=Array[Object]
            )
            Nil
          )
        )
      )
    )
  )
  DefDef( // def <init>(): isabelle.Term_XML$Decode.type in object Term_XML$Decode
    <method>
    "<init>"
    []
    List(Nil)
    <tpt> // tree.tpe=isabelle.Term_XML$Decode.type
    Block( // tree.tpe=Unit
      // 2 statements
      Apply( // def <init>(): Object in class Object, tree.tpe=Object
        Term_XML$Decode.super."<init>" // def <init>(): Object in class Object, tree.tpe=()Object
        Nil
      )
      Assign( // tree.tpe=Unit
        Term_XML$Decode.this."sort " // private[this] val sort: Function1 in object Term_XML$Decode, tree.tpe=Function1
        Apply( // def list(f: Function1): Function1 in object XML$Decode, tree.tpe=Function1
          "isabelle"."XML$Decode"."list" // def list(f: Function1): Function1 in object XML$Decode, tree.tpe=(f: Function1)Function1
          Apply( // val string(): Function1 in object XML$Decode, tree.tpe=Function1
            "isabelle"."XML$Decode"."string" // val string(): Function1 in object XML$Decode, tree.tpe=()Function1
            Nil
          )
        )
      )
      ()
    )
  )
)

== Expanded type of tree ==

ConstantType(value = Constant(Tuple2))

uncaught exception during compilation: java.io.IOException
error: File name too long
two errors found
Failed to compile sources
### Building Isabelle/Graphview ...
src/graph_panel.scala:22: error: not found: object XML
    make_tooltip: (JComponent, Int, Int, XML.Body) => String)
                                         ^
src/model.scala:40: error: not found: value XML
  sealed case class Info(name: String, content: XML.Body)
                                                ^
src/model.scala:57: error: not found: value XML
  val decode_graph: XML.Decode.T[Graph] =
                    ^
src/graphview.scala:34: error: not found: value cat_lines
          case _ => error("Bad arguments:\n" + cat_lines(args))
                                               ^
src/main_panel.scala:35: error: not found: value XML
  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
                                                             ^
error: bad symbolic reference. A signature in Pretty.class refers to term XML
in package isabelle which is not available.
It may be completely missing from the current classpath, or the version on
the classpath might be incompatible with the version used when compiling Pretty.class.
error: bad symbolic reference. A signature in Pretty.class refers to term XML
in package isabelle which is not available.
It may be completely missing from the current classpath, or the version on
the classpath might be incompatible with the version used when compiling Pretty.class.
src/model.scala:44: error: not found: value XML
  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
                   ^
src/model.scala:44: error: not found: value XML
  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
                                               ^
src/model.scala:46: error: not found: value XML
    import XML.Decode._
           ^
src/model.scala:48: error: not found: value pair
    val (name, content) = pair(string, x => x)(body)
                          ^
src/model.scala:49: error: type mismatch;
 found   : Any
 required: String
    Info(name, content)
         ^
error: bad symbolic reference. A signature in Graph.class refers to term XML
in package isabelle which is not available.
It may be completely missing from the current classpath, or the version on
the classpath might be incompatible with the version used when compiling Graph.class.
error: bad symbolic reference. A signature in Graph.class refers to term Decode
in value isabelle.XML which is not available.
It may be completely missing from the current classpath, or the version on
the classpath might be incompatible with the version used when compiling Graph.class.
error: bad symbolic reference. A signature in Graph.class refers to term Decode
in value isabelle.XML which is not available.
It may be completely missing from the current classpath, or the version on
the classpath might be incompatible with the version used when compiling Graph.class.
error: bad symbolic reference. A signature in Graph.class refers to term XML
in package isabelle which is not available.
It may be completely missing from the current classpath, or the version on
the classpath might be incompatible with the version used when compiling Graph.class.
src/model.scala:58: error: not found: value XML
    isabelle.Graph.decode(XML.Decode.string, decode_info)
                          ^
src/mutator_event.scala:31: error: not found: value Swing_Thread
    def += (r: Receiver) { Swing_Thread.require(); receivers += r }
                           ^
src/mutator_event.scala:32: error: not found: value Swing_Thread
    def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
                           ^
src/mutator_event.scala:33: error: not found: value Swing_Thread
    def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
                            ^
20 errors found
Failed to compile sources


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.