Re: [isabelle] Vector transpose



On 27/02/18 13:20, Omar Jasim wrote:
> My theory name is different but I think that there are two different
> theories which have the same name "Matrix.thy". The first
> "HOL/Matrix_LP/Matrix.thy" and the second "
> Jordan_Normal_Form/Matrix.thy". 
> 
>     >
>     > exception THEORY raised (line 230 of "context.ML"):
>     >   Duplicate theory name
>     >   {..., Complex, MacLaurin, Complex_Main, Lattice_Algebras, Draft.Matrix}
>     >   {..., Factorial_Ring, Missing_Ring, Module, Ring_Hom,
>     > Jordan_Normal_Form.Matrix}

In Isabelle2017 imports from other sessions should always use the unique
qualified name -- the Prover IDE should actually resolve that correctly
for files opened in the editor as well, i.e. Draft.Matrix should not occur.

I've made a quick test as follows:

  * start Isabelle/jEdit with AFP/thys as session root directory (option
-d on the command line or a suitable entry in ISABELLE_HOME_USER/ROOTS)

  * open theory file $ISABELLE_HOME/src/HOL/Matrix_LP/Matrix.thy
 -- it correctly gets the formal theory name HOL-Matrix_LP.Matrix (e.g.
hover over the entry in the Theories dockable)

  * open theory file $AFP/Jordan_Normal_Form/Matrix.thy -- it correctly
gets the formal theory name Jordan_Normal_Form.Matrix

  * import both into the Scratch theory:

    theory Scratch
      imports "HOL-Matrix_LP.Matrix" "Jordan_Normal_Form.Matrix"
    begin

    This correctly produces the failure:
exception THEORY raised (line 230 of "context.ML"):
  Duplicate theory name
  {..., Factorial_Ring, Missing_Ring, Module, Ring_Hom,
Jordan_Normal_Form.Matrix}
  {..., Complex, MacLaurin, Complex_Main, Lattice_Algebras,
HOL-Matrix_LP.Matrix}

    So no Draft.Matrix to be seen here.


	Makarius




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