<div dir="ltr">Dear Joe,<div> </div><div>Looks like you have done a lot. Thanks!</div><div> </div><div>1) Here is the first problem: I can't import modular theory</div><div> </div><div> # 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 <a href="https://docs.google.com/document/d/1zPFYM09HLJX0LzGiuWPLij4wU6R0r7GgZMcnBDSIM_M/edit?usp=sharing">the hacking doc</a>?Thanks!Robert</div></div><div class="gmail_extra"> <div class="gmail_quote">On 27 October 2015 at 04:04, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 <a href="http://word-def-modular.int" rel="noreferrer" target="_blank">word-def-modular.int</a> 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/<a href="http://word-def-modular.int" rel="noreferrer" target="_blank">word-def-modular.int</a>"; 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 <div class="HOEnZb"><div class="h5"> On Fri, Oct 9, 2015 at 12:43 AM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >>> Dear Joe, >>> >>> Okay, please let me know when it's ready. >>> >>> Thanks >>> Robert >>> >>> On 6 October 2015 at 23:09, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 >>>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 >>>> >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> 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 >>>> >> > <a href="http://int_type.ml" rel="noreferrer" target="_blank">int_type.ml</a> >>>> >> > which is loaded in <a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a>. >>>> >> > >>>> >> > Could you please update this package? >>>> >> > >>>> >> > Thanks! >>>> >> > >>>> >> > Robert >>>> >> > >>>> >> > >>>> >> > On 6 October 2015 at 12:31, Robert White >>>> >> > <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >>>> >> > 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 >>>> >> >> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >>>> >> >> 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 >>>> >> >>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >>>> >> >>> 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> >>>> >> >>>> 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/<a href="http://natural-divides.int" rel="noreferrer" target="_blank">natural-divides.int</a>";; >>>> >> >>>>> import_article "natural-divides.art";; >>>> >> >>>>> >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/stream/<a href="http://stream.int" rel="noreferrer" target="_blank">stream.int</a>";; >>>> >> >>>>> import_article "stream.art";; >>>> >> >>>>> >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/natural-prime/<a href="http://natural-prime.int" rel="noreferrer" target="_blank">natural-prime.int</a>";; >>>> >> >>>>> 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/<a href="http://stream.int" rel="noreferrer" target="_blank">stream.int</a>";; >>>> >> >>>>> import_article "stream.art";; >>>> >> >>>>> >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/probability/<a href="http://probability.int" rel="noreferrer" target="_blank">probability.int</a>";; >>>> >> >>>>> import_article "probability.art";; >>>> >> >>>>> >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/natural-bits/<a href="http://natural-bits.int" rel="noreferrer" target="_blank">natural-bits.int</a>";; >>>> >> >>>>> import_article "natural-bits.art";; >>>> >> >>>>> >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/natural-divides/<a href="http://natural-divides.int" rel="noreferrer" target="_blank">natural-divides.int</a>";; >>>> >> >>>>> import_article "natural-divides.art";; >>>> >> >>>>> >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/modular/<a href="http://modular.int" rel="noreferrer" target="_blank">modular.int</a>";; >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/word/<a href="http://word.int" rel="noreferrer" target="_blank">word.int</a>";; >>>> >> >>>>> extend_the_interpretation >>>> >> >>>>> "opentheory/theories/word10/<a href="http://word10.int" rel="noreferrer" target="_blank">word10.int</a>";; >>>> >> >>>>> 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 >>>> >> >>>>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> 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: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> >> >>>>> > New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> >> >>>>> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: >>>> >> >>>>> > 0652691901 >>>> >> >>>>> > >>>> >> >>>>> > >>>> >> >>>>> > _______________________________________________ >>>> >> >>>>> > opentheory-users mailing list >>>> >> >>>>> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> >> >>>>> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> >> >>>>> > >>>> >> >>>>> >>>> >> >>>>> _______________________________________________ >>>> >> >>>>> opentheory-users mailing list >>>> >> >>>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> >> >>>>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> >> >>>> >>>> >> >>>> >>>> >> >>>> >>>> >> >>>> >>>> >> >>>> -- >>>> >> >>>> >>>> >> >>>> Regards, >>>> >> >>>> Robert >>>> >> >>>> >>>> >> >>>> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> >> >>>> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> >> >>>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>> >> >>>> >>>> >> >>> >>>> >> >>> >>>> >> >>> >>>> >> >>> -- >>>> >> >>> >>>> >> >>> Regards, >>>> >> >>> Robert >>>> >> >>> >>>> >> >>> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> >> >>> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> >> >>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>> >> >>> >>>> >> >> >>>> >> >> >>>> >> >> >>>> >> >> -- >>>> >> >> >>>> >> >> Regards, >>>> >> >> Robert >>>> >> >> >>>> >> >> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> >> >> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> >> >> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>> >> >> >>>> >> > >>>> >> > >>>> >> > >>>> >> > -- >>>> >> > >>>> >> > Regards, >>>> >> > Robert >>>> >> > >>>> >> > New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> >> > New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> >> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>> >> > >>>> >> > >>>> >> > _______________________________________________ >>>> >> > opentheory-users mailing list >>>> >> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> >> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> >> > >>>> >> >>>> >> _______________________________________________ >>>> >> opentheory-users mailing list >>>> >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> >> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> > >>>> > >>>> > >>>> > >>>> > -- >>>> > >>>> > Regards, >>>> > Robert >>>> > >>>> > New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> > New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>> > >>>> > >>>> > _______________________________________________ >>>> > opentheory-users mailing list >>>> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> > >>>> >>>> _______________________________________________ >>>> opentheory-users mailing list >>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>> >>> >>> >>> >>> -- >>> >>> Regards, >>> Robert >>> >>> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>> >>> >>> _______________________________________________ >>> opentheory-users mailing list >>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>> _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> <div> </div>-- <div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div> </div><div>Regards,</div><div>Robert </div><div> </div><div>New homepage at Github: <a href="https://airobert.github.io/" target="_blank">https://airobert.github.io/</a> </div><div>New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl" style="font-size:12.8px" target="_blank">shuai.wang@student.uva.nl</a> </div><div>Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 </div><div> </div></div></div></div></div></div></div></div></div></div></div></div> </div>