4 1= hg download Isabelle: what is downloaded to where ?
5 2= convert cvs: want .hg created at /usr/local/Isabelle2009-1/ FAILED
6 3= setup mercurial with isac + minimal-Isabelle2009-1
7 4= WN-comments from IsaWS09 (Isabelle2009) to Isabelle2009-1
8 5= continue work from old notebook
10 1=================================================================
11 download Isabelle: what is downloaded to where ?
12 # http://isabelle.in.tum.de/repos/isabelle/summary
13 2 months ago Isabelle2009-1 changeset | changelog | files
15 ~/tmp/isab$ hg clone http://isabelle.in.tum.de/repos/isabelle/file/6a973bd43949 isab/
16 requesting all changes
20 added 35358 changesets with 90911 changes to 7004 files
21 updating working directory
22 2780 files updated, 0 files merged, 0 files removed, 0 files unresolved
26 drwxr-xr-x 10 neuper neuper 4096 2010-02-25 09:04 .
27 drwxr-xr-x 4 neuper neuper 4096 2010-02-25 08:59 ..
28 drwxr-xr-x 11 neuper neuper 4096 2010-02-25 09:04 Admin
30 drwxr-xr-x 3 neuper neuper 4096 2010-02-25 09:04 .hg
31 -rw-r--r-- 1 neuper neuper 405 2010-02-25 09:04 .hgignore
32 -rw-r--r-- 1 neuper neuper 1441 2010-02-25 09:04 .hgtags
34 the whole repository is downloaded inside the dir specified as last argument
35 =================================================================
37 2=================================================================
38 convert cvs: want .hg created at /usr/local/Isabelle2009-1/
39 and isac stored at /usr/local/Isabelle2009-1/src/Pure/isac
40 we had: cvs -d :ext:wneuper@soy.ist.intra:/netshares/commons/isac/.cvs checkout isac
42 /home/neuper/tmp$ hg convert wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml /home/neuper/tmp/isac/sml
43 initializing destination /home/neuper/tmp/isac/sml repository
44 wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml does not look like a CVS checkout
46 abort: wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml: missing or unsupported repository
49 /home/neuper/tmp$ hg convert wneuper@soy.ist.intra:/netshares/commons/isac/.cvs /home/neuper/tmp/isac/sml
50 initializing destination /home/neuper/tmp/isac/sml repository
51 wneuper@soy.ist.intra:/netshares/commons/isac/.cvs does not look like a CVS checkout
53 abort: wneuper@soy.ist.intra:/netshares/commons/isac/.cvs: missing or unsupported repository
56 /home/neuper/tmp$ cvs -d :ext:wneuper@pear.ist.intra:/netshares/commons/isac/.cvs checkout isac
58 /home/neuper/tmp$ cvs -d :ext:wneuper@pear.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml checkout /home/neuper/tmp/isac/sml
59 Cannot access /netshares/commons/isac/.cvs/isac/src/sml/CVSROOT
61 STOPPED, AND COPIED CVS-CHECKOUT FILES WITHOUT CVS INTO proto3
62 NOT: /usr/local/Isabelle2009-1/$ hg convert wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml ...
63 =================================================================
65 3=================================================================
66 setup mercurial with isac + minimal-Isabelle2009-1
67 /usr/local/Isabelle2009-1$ hg init
68 /usr/local/Isabelle2009-1$ emacs .hgingonre &
69 /usr/local/Isabelle2009-1$ hg status # shows right ignores
70 /usr/local/Isabelle2009-1$ hg add -I */*/*/*.sml # etc did not work, thus ...
71 /usr/local/Isabelle2009-1$ hg add # ... all files separately ?!?
72 =================================================================
74 4=================================================================
75 copy WN-comments from IsaWS09 (Isabelle2009) to Isabelle2009-1
76 /usr/local/Isabelle2009/src/Pure$ grep -r WN *
77 IsaMakefile:# scaladoc -d classes $(SCALA_FILES) WN090814 IsaDevWorkshop
78 Isar/isar.scala: /* basic editor commands WN090811 unused */
79 Isar/isar.scala://WN suche parser dazu:
80 Isar/isar.scala://WN for these 3 defs see bottom of Pure/System/isar.ML
81 System/isabelle_process.scala://WN see ex-makarius... for calling this directly
82 System/isabelle_process.scala: /*WN used by interrupt, kill, StdinThread!!, StdoutThread??, MessageThread*/
83 System/isabelle_process.scala: /* stdin WN: of SML, where Scala writes to */
84 System/isabelle_process.scala: /* stdout WN of SML, where Scala reads from*/
85 System/isabelle_system.scala://WN after compile-ERROR: value getenv is not a member of package System...
86 System/isabelle_system.scala: private val environment = System.getenv //WN java.lang.System
87 System/isabelle_system.scala: //WN start own: return "poly"
88 System/isar.ML:(* editor model WN: parsers: -- >> !
89 System/isar.ML: WN go from untyped string to typed world.
90 vvv------------------------------ cp to src/Pure/isac-del/ !search code in other files!
91 classes/isabelle/isar.scala: /* basic editor commands WN090811 unused */
92 classes/isabelle/isar.scala://WN suche parser dazu:
93 classes/isabelle/isar.scala://WN for these 3 defs see bottom of Pure/System/isar.ML
94 classes/isabelle/isabelle_process.scala://WN see ex-makarius... for calling this directly
95 classes/isabelle/isabelle_process.scala: /*WN used by interrupt, kill, StdinThread!!, StdoutThread??, MessageThread*/
96 classes/isabelle/isabelle_process.scala: /* stdin WN: of SML, where Scala writes to */
97 classes/isabelle/isabelle_process.scala: /* stdout WN of SML, where Scala reads from*/
98 classes/isabelle/isabelle_system.scala://WN after compile-ERROR: value getenv is not a member of package System...
99 classes/isabelle/isabelle_system.scala: private val environment = System.getenv //WN java.lang.System
100 classes/isabelle/isabelle_system.scala: //WN start own: return "poly"
101 ^^^------------------------------ cp to src/Pure/isac-del/
102 context.ML:WN the essence of the context
103 context.ML:WN only ensures monotonicity etc, not really production code
104 context.ML:(*fake predeclarations WN forward decl.*)
105 conv.ML:WN see Stefan Berhofers talk at IDWS Aug.09
106 tctical.ML:DOES NOT HANDLE TYPE UNKNOWNS.
107 # thm.ML: type deriv (*WN*)
108 # thm.ML: val rep_thm_G:(*WN*) thm ->
109 # thm.ML: val make_thm:(*WN*) cterm -> thm
110 # thm.ML: val assbl_thm:(*WN*) deriv ->
111 # thm.ML:(*structure Thm = WN for error detection*)
112 # thm.ML:fun rep_thm_G (Thm (deriv , args)) = (deriv, args); (*WN*)
113 # thm.ML:fun make_thm raw_ct = (*WN ---vvv *)
114 # thm.ML: (*else if maxidx <> ~1 then (*WN true with matches (?b * v_ = 0)..*)
115 # thm.ML: end; (*WN ---^^^ *)
116 # thm.ML:fun assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop = (*WN*)
117 variable.ML:(** local context data WN annotation im context, see Isab/Isar Impl. Manual **)
118 =================================================================
120 5=================================================================
121 continue work from old notebook
122 # copy thm-WN.ML --> thm.ML
123 # /usr/local/Isabelle2009-1$ sudo mv HOL HOL-orig
124 # /usr/local/Isabelle2009-1$ sudo ./build HOL
125 # copy other (*WN*) to original files