32 |
32 |
33 ./bin/isabelle components -a |
33 ./bin/isabelle components -a |
34 |
34 |
35 ./bin/isabelle jedit -l HOL |
35 ./bin/isabelle jedit -l HOL |
36 |
36 |
37 ./bin/isabelle jedit -b -f #optional: force fresh build of Isabelle/Scala |
|
38 |
|
39 4. Access documentation (bash shell commands): |
37 4. Access documentation (bash shell commands): |
40 |
38 |
41 ./bin/isabelle build_doc -a |
39 ./bin/isabelle build_doc -a |
42 |
40 |
43 ./bin/isabelle doc system |
41 ./bin/isabelle doc system |
46 Introduction |
44 Introduction |
47 ------------ |
45 ------------ |
48 |
46 |
49 Mercurial https://www.mercurial-scm.org belongs to source code |
47 Mercurial https://www.mercurial-scm.org belongs to source code |
50 management systems that follow the so-called paradigm of "distributed |
48 management systems that follow the so-called paradigm of "distributed |
51 version control". This means plain revision control without the |
49 version control". This means plain versioning without the legacy of |
52 legacy of CVS or SVN (and without the extra complexity introduced by |
50 SVN and the extra complexity of GIT. See also |
53 git). See also http://hginit.com/ for an introduction to the main |
51 https://www.mercurial-scm.org/learn |
54 ideas. The Mercurial book http://hgbook.red-bean.com/ explains many |
|
55 more details. |
|
56 |
52 |
57 Mercurial offers some flexibility in organizing the flow of changes, |
53 Mercurial offers some flexibility in organizing the flow of changes, |
58 both between individual developers and designated pull/push areas that |
54 both between individual developers and designated pull/push areas that |
59 are shared with others. This additional freedom demands additional |
55 are shared with others. This additional freedom demands additional |
60 responsibility to maintain a certain development process that fits to |
56 responsibility to maintain a certain development process that fits to |
98 There is also $HOME/.hgrc for per-user Mercurial configuration. The |
94 There is also $HOME/.hgrc for per-user Mercurial configuration. The |
99 initial configuration requires at least an entry to identify yourself |
95 initial configuration requires at least an entry to identify yourself |
100 as follows: |
96 as follows: |
101 |
97 |
102 [ui] |
98 [ui] |
103 username = XXX |
99 username = ABC |
104 |
100 |
105 Isabelle contributors are free to choose either a short "login name" |
101 Isabelle contributors are free to choose either a short "login name" |
106 (for accounts at TU Munich) or a "full name" -- with or without mail |
102 (for accounts at TU Munich) or a "full name" -- with or without mail |
107 address. It is important to stick to this choice once and for all. |
103 address. It is important to stick to this choice once and for all. |
108 The machine default that Mercurial produces for unspecified |
104 The machine default that Mercurial produces for unspecified |
134 regular mechanisms of Mercurial to report changes upstream, say via |
130 regular mechanisms of Mercurial to report changes upstream, say via |
135 mail to someone with write access to that file space. It is also |
131 mail to someone with write access to that file space. It is also |
136 quite easy to publish changed clones again on the web, using the |
132 quite easy to publish changed clones again on the web, using the |
137 ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts |
133 ad-hoc command "hg serve -v", or the hgweb.cgi or hgwebdir.cgi scripts |
138 that are included in the Mercurial distribution, and send a "pull |
134 that are included in the Mercurial distribution, and send a "pull |
139 request" to someone else. There are also public hosting services for |
135 request" to someone else. |
140 Mercurial repositories, notably Bitbucket. |
|
141 |
136 |
142 The downstream/upstream mode of operation is quite common in the |
137 The downstream/upstream mode of operation is quite common in the |
143 distributed version control community, and works well for occasional |
138 distributed version control community, and works well for occasional |
144 changes produced by anybody out there. Of course, upstream |
139 changes produced by anybody out there. Of course, upstream |
145 maintainers need to review and moderate changes being proposed, before |
140 maintainers need to review and moderate changes being proposed, before |