Difference between pages "Rodin Index Design" and "Help:Preferences"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
m (wrong relational operator)
 
imported>Mathieu
m (importing help from mediawiki)
 
Line 1: Line 1:
==Purpose==
 
  
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences.  This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.
 
  
==Specification==
+
Clicking on the [[special:preferences|my preferences]] link in the upper right while logged in allows you to change your preferences. You will be presented with the User profile section, as well as a bar of tabs across the top for changing other types of settings.
  
===The name table===
+
==User profile==
 +
===User profile===
 +
* ''Username'': Your user name. Only bureaucrats can change your username, and the wiki must also have the [[mw:Extension:Renameuser|Renameuser extension]] installed.
 +
* ''User ID'': A number assigned to your account when you created it (for example, if your number is 42 you are the 42nd user to sign up at this particular wiki). This number is used for internal purposes.
 +
* ''Number of edits'': How many edits you have made. Not all wikis will have this.
 +
* ''Real name'': If provided, this will be used for attribution (rather than using your username). Providing your real name is entirely optional. Some wikis do not have this option.
 +
* ''E-mail'': Your email address, if you have supplied one. You can also change or remove your address here.
 +
* ''Nickname'': When you sign your name (using <code><nowiki>~~~~</nowiki></code>), what you enter here will be used at the start instead of a simple link to your user page. By default, anything you enter here will be wrapped with <code><nowiki>[[ ]]</nowiki></code>; if you want to use special linking, enable ''Raw signatures (without automatic link)''.
 +
* ''Language'': This controls what language the interface is displayed in.  MediaWiki's default interface includes localisations for all supported languages, but this is not necessarily the case with extensions or custom skins. Page text will '''not''' be translated, nor will templates (unless the templates integrate text localisation).
  
Firstly, the index manager needs to store declarations. We make the assumption that a declaration corresponds to one and only one element in the database.
+
===Change password===
 +
To change your password, enter your old password in the first box and your new password in the last two. If you want this site to remember your login, check ''Remember my login on this computer''. Note that this function requires you to have cookies enabled in your browser, and if your cookie is cleared or expires you will no longer be remembered.
  
<blockquote><em>For event-B, this assumption is true. For instance, a variable declaration is an <tt>IVariable</tt> element, an event declaration is an <tt>IEvent</tt>, etc.</em></blockquote>
+
===E-mail===
 +
If you have supplied an email address, you will need to click the ''verify address'' button in order to use these functions. You will receive an email; simply open it and follow the link to enable the following functions.
  
However, the element handle doesn't carry directly the user-defined name for the element.  This name is stored in an attribute of the element.  Thus, one needs to access to the element in the database to retrieve this name.  We therefore want to cache this name in the index to prevent frequent accesses to the database that would hinder performance.
+
* ''E-mail me when a page I'm watching is changed''
 +
* ''E-mail me when my user talk page is changed''
 +
* ''E-mail me also for minor edits of pages''
 +
* ''Enable e-mail from other users''
 +
* ''Send me copies of emails I send to other users''
  
<blockquote>the user-defined name of a variable is stored in its <tt>identifier</tt> attribute, the name of an event in its <tt>label</tt> attribute.</blockquote>
+
===Languages===
  
So, the first table that the index manager needs to maintain is specified as
+
From your preferences you can select what language you would like the interface to be in. Only the buttons like 'edit' and 'talk', in addition to a few pages in the sidebar, will be affected. The main text of the pages will not be changed by this for the vast majority of pages, although there are a few pages where it will, like some in the Wikimedia Meta Wiki.
  
<blockquote><math>\mathit{name}\in\mathit{ELEMENT}\pfun\mathit{STRING}</math>&nbsp;,</blockquote>
+
==Skin==
 +
Here you can choose the skin you want to use (use ''Preview'' if you want to see a skin before you choose it). By default, MediaWiki includes the following skins:
 +
* Chick
 +
* Classic
 +
* Cologne Blue
 +
* MonoBook (default)
 +
* MySkin
 +
* Nostalgia
 +
* Simple
 +
While you can choose whatever skin you like, bear in mind that some wikis will incorporate templates or layout elements that will not display as intended in some of these skins. Generally speaking, sticking with MonoBook (or whatever the wiki's default skin is) will ensure you see pages as intended.
  
where <math>\mathit{ELEMENT}</math> is the set of all element handles and <math>\mathit{STRING}</math> is the set of all character strings.
+
==Math==
 +
Here you can control how mathematical equations described using the <code><nowiki><math></nowiki></code> tag will be displayed. Mathematical formulae uploaded as images or written outside the math tag will not be affected by this setting.
 +
* ''Always render PNG''
 +
* ''HTML if very simple or else PNG''
 +
* ''HTML if possible or else PNG''
 +
* ''Leave it as TeX (for text browsers)''
 +
* ''Recommended for modern browsers''
 +
* ''MathML if possible (experimental)''
  
 +
==Files==
 +
Here you can determine how images will be displayed. Images displayed by direct pasting of a URL (if the wiki has it enabled) will not be affected by this setting.
  
===The occurrences table===
+
* ''Limit images on image description pages to'': This setting lets you choose how big image previews will be on the Image: pages. If you know what your current screen resolution is you may like to set this to one or two sizes smaller than your own screen. If you have a slow connection (such as dial-up) you may want to limit them to 320×240.
 +
* ''Thumbnail size'': Define how big you want thumbnails to appear. This setting will not affect thumbnails with dimensions determined by an editor, nor can it increase images beyond their original dimensions.
  
Secondly, the index manager needs to maintain the relation between declarations and occurrences.  This relation is specified as
+
==Date and time==
 +
The following is normally rendered depending on preferences:
  
<blockquote><math>\mathit{occurrences}\in\dom(\mathit{name})\rel\mathit{LOCATION}</math>&nbsp;,</blockquote>
+
<pre>
 +
[[2001-01-05]] (or [[2001]]-[[01-05]]) (with leading zeros)
 +
[[2001]] [[January 5]] ([[2001]] [[January 05]])
 +
[[January 5]], [[2001]] ([[January 05]], [[2001]])
 +
[[5 January]] [[2001]] ([[05 January]] [[2001]])
 +
[[January 5]] ([[January 05]])
 +
[[5 January]] ([[05 January]])
 +
</pre>
  
where <math>\mathit{LOCATION}</math> is the set of all locations in the database, a location being either an element, or an attribute of an element, or a substring of an attribute of an element.  We also have the following function which relates a location to the element that contains the location
+
With your current preference setting on this project the seven are rendered as follows:
  
<blockquote><math>\mathit{element}\in\mathit{LOCATION}\tsur\mathit{ELEMENT}</math>&nbsp;.</blockquote>
+
#[[2001-01-05]] ([[2001]]-[[01-05]])
 +
#[[2001]] [[January 5]] ([[2001]] [[January 05]])
 +
#[[January 5]], [[2001]] ([[January 05]], [[2001]])
 +
#[[5 January]] [[2001]] ([[05 January]] [[2001]])
 +
#[[January 5]] ([[January 05]])
 +
#[[5 January]] ([[05 January]])
  
However, note that this relation is <em>not</em> maintained by the index manager, it is inherent to the definition of locations.
+
The user-specified date format does not seem to work on the [[mw:]] wiki for links! It works in Recent Changes etc.
  
==Populating the Index==
+
==Editing==
 +
Settings to control editing pages, including the size of the edit box displayed and whether to watch pages that you have edited or created automatically.
  
Following the general principles of the Rodin core, the Rodin index manager is notation agnostic. Therefore, it cannot populate the index by itself, but delegates this to plug-ins through an extension point. These contributions are called <em>indexers</em>.
+
==Recent changes==
 +
* ''Days to show in recent changes'': Here you can specify how far back the [[Help:Tracking changes|recent changes]] pages will go. Note that the list will stop prematurely if the number of edits is exceeded (see below)
 +
* ''Number of edits to show in recent changes'': Here you can specify how many edits should be displayed.
 +
* ''Hide minor edits in recent changes'': This enables you to hide edits marked as minor (see [[Help:Editing pages]]). Since some users will rapidly make a lot of tiny tweaks to update templates or fix spelling errors you may find enabling this to be useful. You can also turn this on temporarily from the recent changes page (see [[Help:Tracking changes]]).
 +
* ''Enhanced recent changes (JavaScript)'': Enhanced recent changes condenses edits into a per-page list. As indicated, this requires JavaScript to be enabled. See [[Help:Tracking changes]] for more information on this feature.
  
Then, the question arises to define the granularity at which these indexers will be declared and work.  Having an indexer declared and working on a whole project would be too coarse grain.  Conversely, having an indexer declared and working at the granularity of internal elements would be too fine grain.  So, it has been decided that indexers are declared for file elements, based on their type. In hindsight, we are taking here the same design decision we took for the event-B tools when defining the granularity of static checking and proof obligation generation.
+
==Watchlist==
  
Moreover, we want to keep the index at least as open as the Rodin database. So, we need to be prepared to accommodate several indexers working on the same file, as the elements contained in a file can be contributed by several plug-insIn this case, the side question is in which order should these indexers be run.  The solution chosen is that any indexer can declare that it should be run after another indexer.  In other words, plug-ins can define a partial order among the indexers that will be enforced by the index manager.
+
==Search==
 +
Default settings for searches including how many results to display and how much context to show for each result.  Check the boxes next to the namespaces which you want to show up, the first time that you search for somethingYou can override this when doing an actual search, by checking or unchecking the boxes at the bottom of the search results screen.
  
Putting everything together, we obtain an extension point for contributing indexers with the following components
+
''Administrators'': To change the namespace default preferences for new users (or users who haven't changed their preferences yet), see [[Manual:$wgNamespacesToBeSearchedDefault]]
  
* id: unique identifier of the indexer
+
==Misc==
* name: human-readable name of the indexer
+
Other settings such as numbering and justification.
* class: implementation of the indexer
 
* type: list of the file element types handled by the indexer
 
* after: list of the ids of the indexers that must be run before the indexer
 
  
 +
== See also ==
 +
* [[Help:Skins]]
  
==Index Maintenance==
+
[[Category:Help|Preferences]]
 
 
Of course, the database will change when users edit their models.  We therefore must define a policy for updating the index when the database is modified.  Detecting database changes is easy, thanks to the deltas that are generated by the database manager upon modification.
 
 
 
The difficulty here is that there is no restriction on the occurrences of an element: an element can occur in the file where it is declared, but it can also occur in a completely different file.
 
 
 
<blockquote>For instance, in event-B, a constant can occur in the context where it is declared, but also in any context that extends (directly or indirectly) its declaring context.</blockquote>
 
 
 
So, in principle, each time a file changes, we have to re-index all files.  This is clearly not acceptable from a performance point of view.  In order to keep index updating efficient, we need to better organize the way file changes are propagated in the index.  For this, we first need to gather additional information from indexers (like dependencies between files), then we have to enforce some restrictions on the indexes contributed by indexers, so that we can compute the consequences of a file change.
 
 
 
===Dependencies===
 
 
 
Firstly, we ask the indexers to provide the index manager with the list of files that a given file depends on.  This is stored in the table with the following specification
 
 
 
<blockquote><math>\mathit{dependsOn}\in\mathit{FILE}\rel\mathit{FILE}</math>&nbsp;,</blockquote>
 
 
 
where <math>\mathit{FILE}</math> is the set of all files.
 
 
 
{{TODO| What happens if <math>\mathit{dependsOn}</math> contains a cycle?}}
 
 
 
But having these dependencies is not precise enough, and can still lead to a lot of unnecessary indexing.
 
 
 
<blockquote>For instance, in event-B, if the user adds a theorem to a context on which all files of a project depend (e.g., the context seen by the top-level machine of this project), then we would have to re-index all the files of the project, although it will be useless, as the theorem is not visible to the other files.</blockquote>
 
 
 
Therefore, we also ask that the indexer reports the declarations that are exported (i.e., made visible)  by a file to the files that depend on it.  This information is stored in the table specified as
 
 
 
<blockquote><math>\mathit{exports}\in\mathit{FILE}\rel\mathit{ELEMENT}</math>&nbsp;.</blockquote>
 
<!--blockquote><math>\mathit{exports}\in\mathit{FILE}\rel(\mathit{ELEMENT}\cprod\mathit{STRING})</math>&nbsp;.</blockquote-->
 
 
 
 
 
===Restrictions===
 
 
 
Then, to minimize re-indexing, we ask that indexers behave as good citizens and enforce some restrictions on the elements and locations that an indexer can contribute to the index.
 
 
 
To express these constraints, we need a new constant relation that gives the file in which an element is declared
 
 
 
<blockquote><math>\mathit{file}\in\mathit{ELEMENT}\rel\mathit{FILE}</math>&nbsp;.</blockquote>
 
 
 
This relation is a constant and is inherent to the database structure, it is not maintained by the index manager, only used by it.
 
 
 
Firstly, we ask that an indexer running on file <math>f</math> contributes names only for elements belonging to this file, i.e., these elements must belong to set
 
 
 
<blockquote><math>
 
  \mathit{file}^{-1}[\{f\}]
 
</math>&nbsp;.</blockquote>
 
 
 
Secondly, the indexer must contribute only occurrences in file <math>f</math>, that is the occurrences provided by an indexer must belong to the set
 
 
 
<blockquote><math>
 
  (\mathit{element}\fcomp\mathit{file})^{-1}[\{f\}]
 
</math>&nbsp;.</blockquote>
 
 
 
Thirdly, an indexer only contributes occurrences for elements declared in the file on which it is run or exported by a file on which this file depends directly, i.e., the elements for which an indexer contributes an occurrence must belong to the set
 
 
 
<blockquote><math>
 
  \mathit{file}^{-1}[\{f\}]\bunion
 
  (\mathit{dependsOn}\fcomp\mathit{exports})[\{f\}]
 
</math>&nbsp;.</blockquote>
 
 
 
Finally, an indexer can only export elements for which it can contribute occurrences, as detailed in the previous point.
 
 
 
 
 
===Updating algorithm===
 
 
 
Given these restrictions, we need to update the index for a file only if
 
* either the file has changed,
 
* or the elements visible in the file have changed
 
since the last time it was indexed.
 
 
 
Formally, the last property means that the following set has changed
 
 
 
<blockquote><math>
 
  (\mathit{dependsOn}\fcomp\mathit{exports})[\{f\}]\domres\mathit{name}
 
</math>&nbsp;.</blockquote>
 
 
 
==Concurrency==
 
 
 
{{TODO|Describe concurrency issues: concurrent access and modifications}}
 
 
 
==Persistence==
 
 
 
{{TODO|How is the indexed made persistent across sessions?}}
 
 
 
[[Category:Design]]
 

Latest revision as of 08:56, 5 July 2008


Clicking on the my preferences link in the upper right while logged in allows you to change your preferences. You will be presented with the User profile section, as well as a bar of tabs across the top for changing other types of settings.

User profile

User profile

  • Username: Your user name. Only bureaucrats can change your username, and the wiki must also have the Renameuser extension installed.
  • User ID: A number assigned to your account when you created it (for example, if your number is 42 you are the 42nd user to sign up at this particular wiki). This number is used for internal purposes.
  • Number of edits: How many edits you have made. Not all wikis will have this.
  • Real name: If provided, this will be used for attribution (rather than using your username). Providing your real name is entirely optional. Some wikis do not have this option.
  • E-mail: Your email address, if you have supplied one. You can also change or remove your address here.
  • Nickname: When you sign your name (using ~~~~), what you enter here will be used at the start instead of a simple link to your user page. By default, anything you enter here will be wrapped with [[ ]]; if you want to use special linking, enable Raw signatures (without automatic link).
  • Language: This controls what language the interface is displayed in. MediaWiki's default interface includes localisations for all supported languages, but this is not necessarily the case with extensions or custom skins. Page text will not be translated, nor will templates (unless the templates integrate text localisation).

Change password

To change your password, enter your old password in the first box and your new password in the last two. If you want this site to remember your login, check Remember my login on this computer. Note that this function requires you to have cookies enabled in your browser, and if your cookie is cleared or expires you will no longer be remembered.

E-mail

If you have supplied an email address, you will need to click the verify address button in order to use these functions. You will receive an email; simply open it and follow the link to enable the following functions.

  • E-mail me when a page I'm watching is changed
  • E-mail me when my user talk page is changed
  • E-mail me also for minor edits of pages
  • Enable e-mail from other users
  • Send me copies of emails I send to other users

Languages

From your preferences you can select what language you would like the interface to be in. Only the buttons like 'edit' and 'talk', in addition to a few pages in the sidebar, will be affected. The main text of the pages will not be changed by this for the vast majority of pages, although there are a few pages where it will, like some in the Wikimedia Meta Wiki.

Skin

Here you can choose the skin you want to use (use Preview if you want to see a skin before you choose it). By default, MediaWiki includes the following skins:

  • Chick
  • Classic
  • Cologne Blue
  • MonoBook (default)
  • MySkin
  • Nostalgia
  • Simple

While you can choose whatever skin you like, bear in mind that some wikis will incorporate templates or layout elements that will not display as intended in some of these skins. Generally speaking, sticking with MonoBook (or whatever the wiki's default skin is) will ensure you see pages as intended.

Math

Here you can control how mathematical equations described using the <math> tag will be displayed. Mathematical formulae uploaded as images or written outside the math tag will not be affected by this setting.

  • Always render PNG
  • HTML if very simple or else PNG
  • HTML if possible or else PNG
  • Leave it as TeX (for text browsers)
  • Recommended for modern browsers
  • MathML if possible (experimental)

Files

Here you can determine how images will be displayed. Images displayed by direct pasting of a URL (if the wiki has it enabled) will not be affected by this setting.

  • Limit images on image description pages to: This setting lets you choose how big image previews will be on the Image: pages. If you know what your current screen resolution is you may like to set this to one or two sizes smaller than your own screen. If you have a slow connection (such as dial-up) you may want to limit them to 320×240.
  • Thumbnail size: Define how big you want thumbnails to appear. This setting will not affect thumbnails with dimensions determined by an editor, nor can it increase images beyond their original dimensions.

Date and time

The following is normally rendered depending on preferences:

 [[2001-01-05]] (or [[2001]]-[[01-05]]) (with leading zeros)
 [[2001]] [[January 5]] ([[2001]] [[January 05]])
 [[January 5]], [[2001]] ([[January 05]], [[2001]])
 [[5 January]] [[2001]] ([[05 January]] [[2001]])
 [[January 5]] ([[January 05]])
 [[5 January]] ([[05 January]])

With your current preference setting on this project the seven are rendered as follows:

  1. 2001-01-05 (2001-01-05)
  2. 2001 January 5 (2001 January 05)
  3. January 5, 2001 (January 05, 2001)
  4. 5 January 2001 (05 January 2001)
  5. January 5 (January 05)
  6. 5 January (05 January)

The user-specified date format does not seem to work on the mw: wiki for links! It works in Recent Changes etc.

Editing

Settings to control editing pages, including the size of the edit box displayed and whether to watch pages that you have edited or created automatically.

Recent changes

  • Days to show in recent changes: Here you can specify how far back the recent changes pages will go. Note that the list will stop prematurely if the number of edits is exceeded (see below)
  • Number of edits to show in recent changes: Here you can specify how many edits should be displayed.
  • Hide minor edits in recent changes: This enables you to hide edits marked as minor (see Help:Editing pages). Since some users will rapidly make a lot of tiny tweaks to update templates or fix spelling errors you may find enabling this to be useful. You can also turn this on temporarily from the recent changes page (see Help:Tracking changes).
  • Enhanced recent changes (JavaScript): Enhanced recent changes condenses edits into a per-page list. As indicated, this requires JavaScript to be enabled. See Help:Tracking changes for more information on this feature.

Watchlist

Search

Default settings for searches including how many results to display and how much context to show for each result. Check the boxes next to the namespaces which you want to show up, the first time that you search for something. You can override this when doing an actual search, by checking or unchecking the boxes at the bottom of the search results screen.

Administrators: To change the namespace default preferences for new users (or users who haven't changed their preferences yet), see Manual:$wgNamespacesToBeSearchedDefault

Misc

Other settings such as numbering and justification.

See also