changeset 66671 41b64e53b6a1
parent 66576 7d4da1c62de7
child 66737 2edc0c42c883
equal deleted inserted replaced
66670:e5188cb1c3d8 66671:41b64e53b6a1
   438   Inform about the status of all sessions required for AFP, without building
   438   Inform about the status of all sessions required for AFP, without building
   439   anything yet:
   439   anything yet:
   440   @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
   440   @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
   441 \<close>
   441 \<close>
   444 section \<open>Maintain theory imports wrt.\ session structure\<close>
   446 text \<open>
   447   The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
   448   session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
   449   \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
   450 \<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
   452   Options are:
   453     -D DIR       include session directory and select its sessions
   454     -I           operation: report potential session imports
   455     -M           operation: Mercurial repository check for theory files
   456     -R           operate on requirements of selected sessions
   457     -U           operation: update theory imports to use session qualifiers
   458     -X NAME      exclude sessions from group NAME and all descendants
   459     -a           select all sessions
   460     -d DIR       include session directory
   461     -g NAME      select session group NAME
   462     -i           incremental update according to session graph structure
   463     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   464     -v           verbose
   465     -x NAME      exclude session NAME and all descendants
   467   Maintain theory imports wrt. session structure. At least one operation
   468   needs to be specified (see options -I -M -U).\<close>}
   470   \<^medskip>
   471   The selection of sessions and session directories works as for @{tool build}
   472   via options \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
   473   \secref{sec:tool-build}).
   475   \<^medskip>
   476   Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
   477   (see \secref{sec:tool-build}).
   479   \<^medskip>
   480   Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
   482   \<^medskip>
   483   Option \<^verbatim>\<open>-I\<close> determines potential session imports, which may be turned into
   484   \isakeyword{sessions} within the corresponding \<^verbatim>\<open>ROOT\<close> file entry. Thus
   485   theory imports from other sessions may use session-qualified names. For
   486   example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> may become formal
   487   \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
   488   \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
   490   \<^medskip>
   491   Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
   492   the underlying session directories; non-repository directories are ignored.
   493   This helps to find files that are accidentally ignored, e.g.\ due to
   494   rearrangements of the session structure.
   496   \<^medskip>
   497   Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
   498   to canonical session-qualified theory names, according to the theory name
   499   space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
   501   Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
   502   following to the session graph structure in bottom-up order. This may
   503   lead to more accurate results in complex session hierarchies.
   504 \<close>
   506 subsubsection \<open>Examples\<close>
   508 text \<open>
   509   Determine potential session imports for some project directory:
   510   @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
   512   \<^smallskip>
   513   Mercurial repository check for some project directory:
   514   @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
   516   \<^smallskip>
   517   Incremental update of theory imports for some project directory:
   518   @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
   519 \<close>
   443 end
   521 end