|
1 src/Pure/isac/README |
|
2 WN100220 |
|
3 |
|
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 |
|
9 |
|
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 |
|
14 ^^^^^^6a973bd43949 |
|
15 ~/tmp/isab$ hg clone http://isabelle.in.tum.de/repos/isabelle/file/6a973bd43949 isab/ |
|
16 requesting all changes |
|
17 adding changesets |
|
18 adding manifests |
|
19 adding file 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 |
|
23 |
|
24 ~/tmp/isab$ ls -la |
|
25 total 404 |
|
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 |
|
29 [...] |
|
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 |
|
33 [...] |
|
34 the whole repository is downloaded inside the dir specified as last argument |
|
35 ================================================================= |
|
36 WN100225 |
|
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 |
|
41 test 1: |
|
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 |
|
45 [...] |
|
46 abort: wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml: missing or unsupported repository |
|
47 |
|
48 test 2: |
|
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 |
|
52 [...] |
|
53 abort: wneuper@soy.ist.intra:/netshares/commons/isac/.cvs: missing or unsupported repository |
|
54 |
|
55 test 3: |
|
56 /home/neuper/tmp$ cvs -d :ext:wneuper@pear.ist.intra:/netshares/commons/isac/.cvs checkout isac |
|
57 OK! |
|
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 |
|
60 |
|
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 ================================================================= |
|
64 |
|
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 ================================================================= |
|
73 |
|
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 ================================================================= |
|
119 |
|
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 |