src/Pure/isac/README

WN100220

1= hg download Isabelle: what is downloaded to where ?

2= convert cvs: want .hg created at /usr/local/Isabelle2009-1/  FAILED

3= setup mercurial with isac  +  minimal-Isabelle2009-1

4= WN-comments from IsaWS09 (Isabelle2009) to Isabelle2009-1

5= continue work from old notebook

1=================================================================

download Isabelle: what is downloaded to where ?

# http://isabelle.in.tum.de/repos/isabelle/summary

          2 months ago	Isabelle2009-1	changeset | changelog | files

														^^^^^^6a973bd43949

~/tmp/isab$ hg clone http://isabelle.in.tum.de/repos/isabelle/file/6a973bd43949  isab/

requesting all changes

adding changesets

adding manifests

adding file changes  

added 35358 changesets with 90911 changes to 7004 files

updating working directory

2780 files updated, 0 files merged, 0 files removed, 0 files unresolved

~/tmp/isab$ ls -la

total 404

drwxr-xr-x 10 neuper neuper   4096 2010-02-25 09:04 .

drwxr-xr-x  4 neuper neuper   4096 2010-02-25 08:59 ..

drwxr-xr-x 11 neuper neuper   4096 2010-02-25 09:04 Admin

[...]

drwxr-xr-x  3 neuper neuper   4096 2010-02-25 09:04 .hg

-rw-r--r--  1 neuper neuper    405 2010-02-25 09:04 .hgignore

-rw-r--r--  1 neuper neuper   1441 2010-02-25 09:04 .hgtags

[...]

the whole repository is downloaded inside the dir specified as last argument

=================================================================

WN100225

2=================================================================

convert cvs: want .hg created at /usr/local/Isabelle2009-1/ 

                     and isac stored at   /usr/local/Isabelle2009-1/src/Pure/isac

we had: cvs -d :ext:wneuper@soy.ist.intra:/netshares/commons/isac/.cvs checkout isac

test 1:

/home/neuper/tmp$ hg convert wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml   /home/neuper/tmp/isac/sml

initializing destination /home/neuper/tmp/isac/sml repository

wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml does not look like a CVS checkout

[...]

abort: wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml: missing or unsupported repository

test 2:

/home/neuper/tmp$ hg convert wneuper@soy.ist.intra:/netshares/commons/isac/.cvs   /home/neuper/tmp/isac/sml

initializing destination /home/neuper/tmp/isac/sml repository

wneuper@soy.ist.intra:/netshares/commons/isac/.cvs does not look like a CVS checkout

[...]

abort: wneuper@soy.ist.intra:/netshares/commons/isac/.cvs: missing or unsupported repository

test 3: 

/home/neuper/tmp$ cvs -d :ext:wneuper@pear.ist.intra:/netshares/commons/isac/.cvs checkout isac

OK!

/home/neuper/tmp$ cvs -d :ext:wneuper@pear.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml  checkout   /home/neuper/tmp/isac/sml

Cannot access /netshares/commons/isac/.cvs/isac/src/sml/CVSROOT

STOPPED, AND COPIED CVS-CHECKOUT FILES WITHOUT CVS INTO proto3

NOT: /usr/local/Isabelle2009-1/$ hg convert wneuper@soy.ist.intra:/netshares/commons/isac/.cvs/isac/src/sml  ...

=================================================================

3=================================================================

setup mercurial with isac  +  minimal-Isabelle2009-1

/usr/local/Isabelle2009-1$ hg init

/usr/local/Isabelle2009-1$ emacs .hgingonre &

/usr/local/Isabelle2009-1$ hg status                  # shows right ignores

/usr/local/Isabelle2009-1$ hg add -I */*/*/*.sml  # etc did not work, thus ...

/usr/local/Isabelle2009-1$ hg add                      # ... all files separately ?!?

=================================================================

4=================================================================

copy WN-comments from IsaWS09 (Isabelle2009) to Isabelle2009-1

/usr/local/Isabelle2009/src/Pure$ grep -r WN *

IsaMakefile:#   scaladoc -d classes $(SCALA_FILES)   WN090814 IsaDevWorkshop

Isar/isar.scala:  /* basic editor commands WN090811 unused */

Isar/isar.scala://WN suche parser dazu:

Isar/isar.scala://WN for these 3 defs see bottom of Pure/System/isar.ML

System/isabelle_process.scala://WN see ex-makarius... for calling this directly

System/isabelle_process.scala:  /*WN used by interrupt, kill, StdinThread!!, StdoutThread??, MessageThread*/

System/isabelle_process.scala:  /* stdin WN: of SML, where Scala writes to */

System/isabelle_process.scala:  /* stdout WN of SML, where Scala reads from*/

System/isabelle_system.scala://WN after compile-ERROR: value getenv is not a member of package System...

System/isabelle_system.scala:  private val environment = System.getenv //WN java.lang.System

System/isabelle_system.scala:    //WN start own: return "poly"

System/isar.ML:(* editor model WN: parsers: --  >>  !

System/isar.ML:   WN go from untyped string to typed world.

vvv------------------------------ cp to src/Pure/isac-del/     !search code in other files!

classes/isabelle/isar.scala:  /* basic editor commands WN090811 unused */

classes/isabelle/isar.scala://WN suche parser dazu:

classes/isabelle/isar.scala://WN for these 3 defs see bottom of Pure/System/isar.ML

classes/isabelle/isabelle_process.scala://WN see ex-makarius... for calling this directly

classes/isabelle/isabelle_process.scala:  /*WN used by interrupt, kill, StdinThread!!, StdoutThread??, MessageThread*/

classes/isabelle/isabelle_process.scala:  /* stdin WN: of SML, where Scala writes to */

classes/isabelle/isabelle_process.scala:  /* stdout WN of SML, where Scala reads from*/

classes/isabelle/isabelle_system.scala://WN after compile-ERROR: value getenv is not a member of package System...

classes/isabelle/isabelle_system.scala:  private val environment = System.getenv //WN java.lang.System

classes/isabelle/isabelle_system.scala:    //WN start own: return "poly"

^^^------------------------------ cp to src/Pure/isac-del/

context.ML:WN the essence of the context

context.ML:WN only ensures monotonicity etc, not really production code

context.ML:(*fake predeclarations WN forward decl.*)

conv.ML:WN see Stefan Berhofers talk at IDWS Aug.09

tctical.ML:DOES NOT HANDLE TYPE UNKNOWNS.

# thm.ML:  type deriv (*WN*)

# thm.ML:  val rep_thm_G:(*WN*) thm ->

# thm.ML:  val make_thm:(*WN*) cterm -> thm

# thm.ML:  val assbl_thm:(*WN*) deriv ->

# thm.ML:(*structure Thm =          WN for error detection*)

# thm.ML:fun rep_thm_G (Thm (deriv , args)) = (deriv, args); (*WN*)

# thm.ML:fun make_thm raw_ct =         (*WN  ---vvv *)

# thm.ML:  (*else if maxidx <> ~1 then (*WN true with matches (?b * v_ = 0)..*)

# thm.ML:  end;                        (*WN  ---^^^ *)

# thm.ML:fun assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop = (*WN*)

variable.ML:(** local context data WN annotation im context, see Isab/Isar Impl. Manual **)

=================================================================

5=================================================================

continue work from old notebook

# copy thm-WN.ML --> thm.ML

# /usr/local/Isabelle2009-1$ sudo mv HOL HOL-orig

# /usr/local/Isabelle2009-1$ sudo ./build HOL

# copy other (*WN*) to original files