[opentheory-users] Error loading articles

Robert White ai.robert.wangshuai at gmail.com
Tue Oct 27 21:53:29 UTC 2015
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Dear Joe,

Looks like you have done a lot. Thanks!

1) Here is the first problem: I can't import modular theory

#  import_theory "modular";;

opentheory: unknown switch "--directory"

usage: opentheory info [info options] INPUT

Extract information from packages and files.

Displaying info options:

  --format FORMAT ...... format package information

  --information ........ display all package information

  --theory ............. display the package theory

  --article ............ output the package theory in article format

  --requires ........... list satisfying required packages

  --inference .......... display count of inference rules

  --files .............. list package files

  --document ........... output package document in HTML format

  --theory-source ...... output package theory source

  --theorems ........... output package theorems in article format

  --assumptions ........ output package assumptions in article format

  --symbols ............ list all symbols in the package

  --includes ........... list included packages

  -o, --output FILE .... write previous information to FILE

  --output-version N ... set previous information output version

  --show-assumptions ... do not hide satisfied assumptions

  --show-derivations ... show assumptions and axioms for each theorem

  --upgrade-theory ..... upgrade theory source to latest versions

  --preserve-theory .... do not optimize theory source

  -- ................... no more options

  -?, -h, --help ....... display option information and exit

  -v, --version ........ display version information

INPUT is one of the following:

  - A package: NAME-VERSION or NAME (for the latest version)

  - A theory source file: FILE.thy or theory:FILE

  - A proof article file: FILE.art or article:FILE

  - A package tarball: FILE.tgz or tarball:FILE

  - A package staged for installation: staged:NAME-VERSION

NAME is a package name (e.g., base).

VERSION is a package version (e.g., 1.0).

FILE is a filename; use - to read from stdin or write to stdout.

FORMAT is a string containing {NAME,VERSION,DESCRIPTION,CHECKSUM,EMPTY}.

Exception: Failure "theory_directory: strange output for theory stream".


2) I also noticed that you removed start_logging();; Then how should I
export the proofs. Could you please give me an example or maybe update the
hacking doc
<https://docs.google.com/document/d/1zPFYM09HLJX0LzGiuWPLij4wU6R0r7GgZMcnBDSIM_M/edit?usp=sharing>
?

Thanks!

Robert

On 27 October 2015 at 04:04, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> I have worked a little more on the HOL Light/OpenTheory interface, and
> now include the HOL Light names of theorems in the theory packages, in
> addition to the HOL Light names of type operators and constants. For
> example, the following command results in the theorems in the modular
> theory having Ocaml names just like they'd been proved in an
> interactive session:
>
> # import_theory "modular";;
> auto-imported theory stream : {128} |> {55}
> auto-imported theory probability : {39} |> {18}
> auto-imported theory natural-bits : {205} |> {210}
> auto-imported theory natural-divides : {177} |> {136}
> imported sub-theory modular-witness : {8} |> {1}
> imported theory modular : {75} |> {68}
> val it : Theory.t = modular : {75} |> {68}
> # modular_exp_add;;
> val it : thm =
>   |- !x m n.
>          modular_mult (modular_exp x m) (modular_exp x n) =
>          modular_exp x (m + n)
>
> I have also added an interpret_theory command to "interpret" a theory
> in another context. For example, the following command interprets the
> modular theory inside the word theory, renaming the type operators and
> constants according to the word-def-modular.int file, and renaming the
> theorems by replacing the "modular" with "word" and "modulus" with
> "word_size".
>
> # interpret_theory
>     {Import.source_theory = "modular";
>      Import.interpretation = "opentheory/theories/word/
> word-def-modular.int";
>      Import.theorem_renamer = Import.replace "modular" "word" o
>                               Import.replace "modulus" "word_size";
>      Import.destination_theory = "word-def"};;
> val it : Theory.t = modular : {75} |> {68}
> # word_exp_add;;
> val it : thm =
>   |- !x m n. word_mult (word_exp x m) (word_exp x n) = word_exp x (m + n)
>
> Hopefully this will make it easier to import OpenTheory theories into HOL
> Light.
>
> Cheers,
>
> Joe
>
> On Fri, Oct 9, 2015 at 12:43 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> > Hi Robert,
> >
> > I've worked a little more on the HOL Light import, so now all you need
> > to do is the following:
> >
> > # logfile "test-import";;
> > val it : unit = ()
> > # import_theory "word10";;
> > auto-importing theory stream
> > auto-importing theory probability
> > auto-importing theory natural-bits
> > auto-importing theory natural-divides
> > importing theory word10
> > val it : thm list * thm list = ...
> > # imported_theories ();;
> > val it : string list =
> >   ["base"; "stream"; "probability"; "natural-bits"; "natural-divides";
> >    "word10"]
> >
> > Under the covers it calls the opentheory tool to recursively import
> > all the required theories, extends the interpretation for the new
> > theory, converts the theory into an article with cleared local symbol
> > names, and finally reads the article into HOL Light.
> >
> > Hopefully this should make things a little easier.
> >
> > Cheers,
> >
> > Joe
> >
> > On Thu, Oct 8, 2015 at 1:05 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >> Hi Robert,
> >>
> >> I've just released a new version of the opentheory tool with a new
> >> option that should solve the name clashing problem when importing into
> >> HOL Light. Here's how you use it:
> >>
> >> opentheory info --clear-local-names --article -o parser.art parser
> >>
> >> This replaces the names of all symbols that are local to the theory
> >> with the special empty name (which prints as _). You can see this with
> >> the following command:
> >>
> >> $ opentheory info --symbols parser.art
> >> 7 external type operators: -> bool Data.List.list Data.Option.option
> >>   Data.Pair.* Data.Sum.+ Number.Natural.natural
> >> 46 external constants: = select ! /\ ==> ? ?! \/ ~ cond F T Data.List.::
> >>   Data.List.@ Data.List.[] Data.List.concat Data.List.length
> Data.List.map
> >>   Data.Option.case.none.some Data.Option.map Data.Option.none
> >>   Data.Option.some Data.Pair., Data.Pair.fst Data.Pair.snd
> >>   Data.Sum.case.left.right Data.Sum.left Data.Sum.right Function.const
> >>   Function.o Function.surjective Number.Natural.* Number.Natural.+
> >>   Number.Natural.- Number.Natural.< Number.Natural.<= Number.Natural.^
> >>   Number.Natural.bit0 Number.Natural.bit1 Number.Natural.even
> >>   Number.Natural.suc Number.Natural.zero Relation.irreflexive
> >>   Relation.measure Relation.subrelation Relation.wellFounded
> >> 3 defined type operators: _ Parser.parser Parser.Stream.stream
> >> 59 defined constants: _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
> >>   Parser.any Parser.apply Parser.dest Parser.filter Parser.fold
> >>   Parser.fold.prs Parser.foldN Parser.invariant Parser.inverse
> Parser.map
> >>   Parser.mapPartial Parser.mapPartial.prs Parser.mk Parser.none
> >>   Parser.orelse Parser.orelse.prs Parser.pair Parser.parse
> Parser.sequence
> >>   Parser.sequence.prs Parser.some Parser.strongInverse Parser.token
> >>   Parser.token.prs Parser.Stream.append
> Parser.Stream.case.error.eof.cons
> >>   Parser.Stream.cons Parser.Stream.eof Parser.Stream.error
> >>   Parser.Stream.fromList Parser.Stream.isProperSuffix
> >>   Parser.Stream.isSuffix Parser.Stream.length Parser.Stream.map
> >>   Parser.Stream.toList
> >>
> >> Here you can see there is one occurrence of a local type operator and
> >> many occurrences of local constants. Local symbols are defined and
> >> used internally in the theory but do not appear in any exported
> >> theorem (or assumption).
> >>
> >> It was local symbols that were causing name clashes when importing
> >> theories into HOL Light. I have updated the import mechanism so that
> >> fresh symbol names are generated when an empty name is encountered.
> >> You will need to execute a git pull of the OpenTheory HOL Light fork
> >> to get this update.
> >>
> >> The parser theory now imports without issue, and word10 theory imports
> >> without needing the extra extend_the_interpretation commands
> >> beforehand.
> >>
> >> Please give the new HOL Light import flow a try and let me know of any
> >> problems. It was a bit trickier than expected getting it all to work,
> >> so it wouldn't surprise me if there were issues.
> >>
> >> Cheers,
> >>
> >> Joe
> >>
> >> On Tue, Oct 6, 2015 at 2:22 PM, Robert White
> >> <ai.robert.wangshuai at gmail.com> wrote:
> >>> Dear Joe,
> >>>
> >>> Okay, please let me know when it's ready.
> >>>
> >>> Thanks
> >>> Robert
> >>>
> >>> On 6 October 2015 at 23:09, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>>>
> >>>> No, but you should shortly be able to download a new version of the
> >>>> opentheory tool that will fix it.
> >>>>
> >>>> Cheers,
> >>>>
> >>>> Joe
> >>>>
> >>>> On Tue, Oct 6, 2015 at 2:08 PM, Robert White
> >>>> <ai.robert.wangshuai at gmail.com> wrote:
> >>>> >> This is a case of a theory-local definition clashing with an
> existing
> >>>> > definition of the same name. It will be solved by the same change
> that
> >>>> > I'm working on that will make the extra extend_the_interpretation
> >>>> > commands unnecessary.
> >>>> >
> >>>> > So looks like i can't do anything for now on it?
> >>>> >
> >>>> >
> >>>> >
> >>>> > On 6 October 2015 at 23:04, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>>> >>
> >>>> >> Hi Robert,
> >>>> >>
> >>>> >> This is a case of a theory-local definition clashing with an
> existing
> >>>> >> definition of the same name. It will be solved by the same change
> that
> >>>> >> I'm working on that will make the extra extend_the_interpretation
> >>>> >> commands unnecessary.
> >>>> >>
> >>>> >> Cheers,
> >>>> >>
> >>>> >> Joe
> >>>> >>
> >>>> >> On Tue, Oct 6, 2015 at 4:00 AM, Robert White
> >>>> >> <ai.robert.wangshuai at gmail.com> wrote:
> >>>> >> > Dear Joe,
> >>>> >> >
> >>>> >> > I also noticed that parser is has the following errors:
> >>>> >> >
> >>>> >> > Exception:
> >>>> >> >
> >>>> >> > Failure
> >>>> >> >
> >>>> >> >  "in article parser.art at line 457: defineConst\nstack = [Term;
> >>>> >> > \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var;
> >>>> >> > Term;
> >>>> >> > Var;
> >>>> >> > [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var;
> >>>> >> > \"HOLLight.INJP\";
> >>>> >> > \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term; Var; Term;
> Var;
> >>>> >> > \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\";
> >>>> >> > \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; \"a1\"; Var;
> [\"A\"];
> >>>> >> > \"HOLLight._dest_pstream\"; \"HOLLight._mk_pstream\";
> >>>> >> > \"Parser.Stream.stream\"; TypeOp<fun>; TypeOp<fun>; Const<!>;
> >>>> >> > Term]\nnew_constant: constant NUMSUM has already been declared".
> >>>> >> >
> >>>> >> >
> >>>> >> > I looked into it and found that NUMSUM has been declared in
> >>>> >> > int_type.ml
> >>>> >> > which is  loaded in hol.ml.
> >>>> >> >
> >>>> >> > Could you please update this package?
> >>>> >> >
> >>>> >> > Thanks!
> >>>> >> >
> >>>> >> > Robert
> >>>> >> >
> >>>> >> >
> >>>> >> > On 6 October 2015 at 12:31, Robert White
> >>>> >> > <ai.robert.wangshuai at gmail.com>
> >>>> >> > wrote:
> >>>> >> >>
> >>>> >> >> Dear Joe,
> >>>> >> >>
> >>>> >> >> I also have problem loading lazy-list and gfp:
> >>>> >> >>
> >>>> >> >> For lazy-list :
> >>>> >> >>
> >>>> >> >> Exception:
> >>>> >> >>
> >>>> >> >> Failure
> >>>> >> >>
> >>>> >> >>  "in article lazy-list.art at line 234: const\nstack =
> >>>> >> >> [\"Data.Option.NONE\"; Var; Term; Term; Term; Var; Term; Term;
> Var;
> >>>> >> >> Term;
> >>>> >> >> Var; \"llist.lrep_ok\"; Var; Term; Term; [\"A\"];
> >>>> >> >> \"llist.llist.rep\";
> >>>> >> >> \"llist.llist.abs\"; \"llist.llist\"; \"a0\"; \"llist.LFINITE\";
> >>>> >> >> Var;
> >>>> >> >> Thm;
> >>>> >> >> Thm]\nunknown constant \"Data.Option.NONE\"".
> >>>> >> >>
> >>>> >> >>
> >>>> >> >> For gfp;
> >>>> >> >>
> >>>> >> >>
> >>>> >> >> Exception:
> >>>> >> >>
> >>>> >> >> Failure
> >>>> >> >>
> >>>> >> >>  "in article gfp.art at line 676: axiom\nstack = [Term; []; Thm;
> >>>> >> >> Thm;
> >>>> >> >> Thm]\nunknown assumption:\n|- prime oddprime".
> >>>> >> >>
> >>>> >> >>
> >>>> >> >> Could you please help on that? Thanks a lot!
> >>>> >> >>
> >>>> >> >> Regards
> >>>> >> >>
> >>>> >> >> Robert
> >>>> >> >>
> >>>> >> >>
> >>>> >> >>
> >>>> >> >>
> >>>> >> >>
> >>>> >> >> On 6 October 2015 at 12:15, Robert White
> >>>> >> >> <ai.robert.wangshuai at gmail.com>
> >>>> >> >> wrote:
> >>>> >> >>>
> >>>> >> >>> Dear Joe,
> >>>> >> >>>
> >>>> >> >>> I still get one error from the modular package:
> >>>> >> >>>
> >>>> >> >>> Exception:
> >>>> >> >>>
> >>>> >> >>> Failure
> >>>> >> >>>
> >>>> >> >>>  "in article modular.art at line 11928: axiom\nstack = [Term;
> [];
> >>>> >> >>> Thm;
> >>>> >> >>> Thm; [[]; [[Var; Term]]]; Thm; Thm; Thm; Thm; Thm; Thm; Thm;
> Thm;
> >>>> >> >>> Thm;
> >>>> >> >>> Var;
> >>>> >> >>> Thm; Thm; Thm; Thm; Thm; Var; Thm; Thm; Thm; Thm;
> >>>> >> >>> [[\"Number.Modular.toNatural\"; Var]]; Term; Var; Var;
> >>>> >> >>> \"Number.Modular.<=\"; Term; Var; [[]; [[Var; Term]]]; Var;
> >>>> >> >>> Thm]\nunknown
> >>>> >> >>> assumption:\n|- ~(modulus = 0)".
> >>>> >> >>>
> >>>> >> >>> Is there any package missing?
> >>>> >> >>>
> >>>> >> >>> I have loaded the following packages:
> >>>> >> >>>
> >>>> >> >>> stream
> >>>> >> >>>
> >>>> >> >>> probability
> >>>> >> >>>
> >>>> >> >>> natural-bits
> >>>> >> >>>
> >>>> >> >>> natural-divides
> >>>> >> >>>
> >>>> >> >>> natural-prime
> >>>> >> >>>
> >>>> >> >>>
> >>>> >> >>> Thanks very much!
> >>>> >> >>>
> >>>> >> >>>
> >>>> >> >>> Regards,
> >>>> >> >>>
> >>>> >> >>> Robert
> >>>> >> >>>
> >>>> >> >>>
> >>>> >> >>> On 5 October 2015 at 23:27, Robert White
> >>>> >> >>> <ai.robert.wangshuai at gmail.com>
> >>>> >> >>> wrote:
> >>>> >> >>>>
> >>>> >> >>>> Thanks very much Joe.
> >>>> >> >>>> I also noticed that there is kind of dependency going on but I
> >>>> >> >>>> don't
> >>>> >> >>>> know how to fix it.
> >>>> >> >>>>
> >>>> >> >>>>
> >>>> >> >>>> On 5 October 2015 at 22:56, Joe Leslie-Hurd <joe at gilith.com>
> >>>> >> >>>> wrote:
> >>>> >> >>>>>
> >>>> >> >>>>> Hi Robert,
> >>>> >> >>>>>
> >>>> >> >>>>> There are a couple of different obstacles here.
> >>>> >> >>>>>
> >>>> >> >>>>> Firstly, it is important that the dependent theories have
> been
> >>>> >> >>>>> imported before the theory. To show all the dependent
> theories,
> >>>> >> >>>>> use
> >>>> >> >>>>> the following command:
> >>>> >> >>>>>
> >>>> >> >>>>> $ opentheory list --dependency-order 'Requires+
> natural-prime'
> >>>> >> >>>>> base-1.200
> >>>> >> >>>>> natural-divides-1.62
> >>>> >> >>>>> stream-1.46
> >>>> >> >>>>>
> >>>> >> >>>>> Now this sequence will succeed:
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/natural-divides/natural-divides.int
> ";;
> >>>> >> >>>>> import_article "natural-divides.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/stream/stream.int";;
> >>>> >> >>>>> import_article "stream.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/natural-prime/natural-prime.int";;
> >>>> >> >>>>> import_article "natural-prime.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> The second obstacle is that the theory word10 includes the
> theory
> >>>> >> >>>>> word, which in turn includes the theory modular. So to
> >>>> >> >>>>> successfully
> >>>> >> >>>>> import word10 you need to extend the interpretation with the
> >>>> >> >>>>> interpretations for these theories, too:
> >>>> >> >>>>>
> >>>> >> >>>>> $ opentheory list --dependency-order 'Requires+ word10'
> >>>> >> >>>>> base-1.200
> >>>> >> >>>>> stream-1.46
> >>>> >> >>>>> probability-1.49
> >>>> >> >>>>> natural-bits-1.66
> >>>> >> >>>>> natural-divides-1.62
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/stream/stream.int";;
> >>>> >> >>>>> import_article "stream.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/probability/probability.int";;
> >>>> >> >>>>> import_article "probability.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/natural-bits/natural-bits.int";;
> >>>> >> >>>>> import_article "natural-bits.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/natural-divides/natural-divides.int
> ";;
> >>>> >> >>>>> import_article "natural-divides.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/modular/modular.int";;
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/word/word.int";;
> >>>> >> >>>>> extend_the_interpretation
> >>>> >> >>>>>   "opentheory/theories/word10/word10.int";;
> >>>> >> >>>>> import_article "word10.art";;
> >>>> >> >>>>>
> >>>> >> >>>>> I regard this second problem as a defect in the theories,
> because
> >>>> >> >>>>> it's
> >>>> >> >>>>> unreasonable to expect people to discover this information.
> I'll
> >>>> >> >>>>> work
> >>>> >> >>>>> on fixing it so these multiple extend_the_interpretation
> commands
> >>>> >> >>>>> are
> >>>> >> >>>>> unnecessary.
> >>>> >> >>>>>
> >>>> >> >>>>> Cheers,
> >>>> >> >>>>>
> >>>> >> >>>>> Joe
> >>>> >> >>>>>
> >>>> >> >>>>> On Sun, Oct 4, 2015 at 2:57 PM, Robert White
> >>>> >> >>>>> <ai.robert.wangshuai at gmail.com> wrote:
> >>>> >> >>>>> > Dear Joe,
> >>>> >> >>>>> >
> >>>> >> >>>>> > I have problem importing article files. For example:
> >>>> >> >>>>> >
> >>>> >> >>>>> > Failure
> >>>> >> >>>>> >
> >>>> >> >>>>> >  "in article word10.art at line 7495: defineConst\nstack =
> >>>> >> >>>>> > [Term;
> >>>> >> >>>>> > \"Number.Modular.equivalent\"; Term; Var; Term; Var; [];
> >>>> >> >>>>> > \"HOLLight.modular_to_class\";
> \"HOLLight.modular_from_class\";
> >>>> >> >>>>> > \"Data.Word10.word10\"; TypeOp<fun>; TypeOp<fun>;
> >>>> >> >>>>> > Const<!>]\nunknown
> >>>> >> >>>>> > constant \"Number.Modular.equivalent\"".
> >>>> >> >>>>> >
> >>>> >> >>>>> > I also have problems with the following packages:
> >>>> >> >>>>> >
> >>>> >> >>>>> > natural-prime
> >>>> >> >>>>> >
> >>>> >> >>>>> > gfp
> >>>> >> >>>>> >
> >>>> >> >>>>> > natural-fibonacci
> >>>> >> >>>>> >
> >>>> >> >>>>> > Could you please check if that is because opentheory
> packages
> >>>> >> >>>>> > got
> >>>> >> >>>>> > updated
> >>>> >> >>>>> > but the int files haven't?
> >>>> >> >>>>> >
> >>>> >> >>>>> > Thanks a lot.
> >>>> >> >>>>> >
> >>>> >> >>>>> >
> >>>> >> >>>>> > --
> >>>> >> >>>>> >
> >>>> >> >>>>> > Regards,
> >>>> >> >>>>> > Robert
> >>>> >> >>>>> >
> >>>> >> >>>>> > New homepage at Github: https://airobert.github.io/
> >>>> >> >>>>> > New email address at ILLC: shuai.wang at student.uva.nl
> >>>> >> >>>>> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP:
> >>>> >> >>>>> > 0652691901
> >>>> >> >>>>> >
> >>>> >> >>>>> >
> >>>> >> >>>>> > _______________________________________________
> >>>> >> >>>>> > opentheory-users mailing list
> >>>> >> >>>>> > opentheory-users at gilith.com
> >>>> >> >>>>> > http://www.gilith.com/opentheory/mailing-list
> >>>> >> >>>>> >
> >>>> >> >>>>>
> >>>> >> >>>>> _______________________________________________
> >>>> >> >>>>> opentheory-users mailing list
> >>>> >> >>>>> opentheory-users at gilith.com
> >>>> >> >>>>> http://www.gilith.com/opentheory/mailing-list
> >>>> >> >>>>
> >>>> >> >>>>
> >>>> >> >>>>
> >>>> >> >>>>
> >>>> >> >>>> --
> >>>> >> >>>>
> >>>> >> >>>> Regards,
> >>>> >> >>>> Robert
> >>>> >> >>>>
> >>>> >> >>>> New homepage at Github: https://airobert.github.io/
> >>>> >> >>>> New email address at ILLC: shuai.wang at student.uva.nl
> >>>> >> >>>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP:
> 0652691901
> >>>> >> >>>>
> >>>> >> >>>
> >>>> >> >>>
> >>>> >> >>>
> >>>> >> >>> --
> >>>> >> >>>
> >>>> >> >>> Regards,
> >>>> >> >>> Robert
> >>>> >> >>>
> >>>> >> >>> New homepage at Github: https://airobert.github.io/
> >>>> >> >>> New email address at ILLC: shuai.wang at student.uva.nl
> >>>> >> >>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP:
> 0652691901
> >>>> >> >>>
> >>>> >> >>
> >>>> >> >>
> >>>> >> >>
> >>>> >> >> --
> >>>> >> >>
> >>>> >> >> Regards,
> >>>> >> >> Robert
> >>>> >> >>
> >>>> >> >> New homepage at Github: https://airobert.github.io/
> >>>> >> >> New email address at ILLC: shuai.wang at student.uva.nl
> >>>> >> >> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP:
> 0652691901
> >>>> >> >>
> >>>> >> >
> >>>> >> >
> >>>> >> >
> >>>> >> > --
> >>>> >> >
> >>>> >> > Regards,
> >>>> >> > Robert
> >>>> >> >
> >>>> >> > New homepage at Github: https://airobert.github.io/
> >>>> >> > New email address at ILLC: shuai.wang at student.uva.nl
> >>>> >> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
> >>>> >> >
> >>>> >> >
> >>>> >> > _______________________________________________
> >>>> >> > opentheory-users mailing list
> >>>> >> > opentheory-users at gilith.com
> >>>> >> > http://www.gilith.com/opentheory/mailing-list
> >>>> >> >
> >>>> >>
> >>>> >> _______________________________________________
> >>>> >> opentheory-users mailing list
> >>>> >> opentheory-users at gilith.com
> >>>> >> http://www.gilith.com/opentheory/mailing-list
> >>>> >
> >>>> >
> >>>> >
> >>>> >
> >>>> > --
> >>>> >
> >>>> > Regards,
> >>>> > Robert
> >>>> >
> >>>> > New homepage at Github: https://airobert.github.io/
> >>>> > New email address at ILLC: shuai.wang at student.uva.nl
> >>>> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
> >>>> >
> >>>> >
> >>>> > _______________________________________________
> >>>> > opentheory-users mailing list
> >>>> > opentheory-users at gilith.com
> >>>> > http://www.gilith.com/opentheory/mailing-list
> >>>> >
> >>>>
> >>>> _______________________________________________
> >>>> opentheory-users mailing list
> >>>> opentheory-users at gilith.com
> >>>> http://www.gilith.com/opentheory/mailing-list
> >>>
> >>>
> >>>
> >>>
> >>> --
> >>>
> >>> Regards,
> >>> Robert
> >>>
> >>> New homepage at Github: https://airobert.github.io/
> >>> New email address at ILLC: shuai.wang at student.uva.nl
> >>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
> >>>
> >>>
> >>> _______________________________________________
> >>> opentheory-users mailing list
> >>> opentheory-users at gilith.com
> >>> http://www.gilith.com/opentheory/mailing-list
> >>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>



-- 

Regards,
Robert

New homepage at Github: https://airobert.github.io/
New email address at ILLC: shuai.wang at student.uva.nl
Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151027/63c0896a/attachment-0001.html>
Previous message: [opentheory-users] Error loading articles
Next message: [opentheory-users] Error loading articles
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list