482 anything yet: |
482 anything yet: |
483 @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>} |
483 @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>} |
484 \<close> |
484 \<close> |
485 |
485 |
486 |
486 |
487 section \<open>Maintain theory imports wrt.\ session structure\<close> |
|
488 |
|
489 text \<open> |
|
490 The @{tool_def "imports"} tool helps to maintain theory imports wrt.\ |
|
491 session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>, |
|
492 \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display] |
|
493 \<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...] |
|
494 |
|
495 Options are: |
|
496 -B NAME include session NAME and all descendants |
|
497 -D DIR include session directory and select its sessions |
|
498 -I operation: report session imports |
|
499 -M operation: Mercurial repository check for theory files |
|
500 -R operate on requirements of selected sessions |
|
501 -U operation: update theory imports to use session qualifiers |
|
502 -X NAME exclude sessions from group NAME and all descendants |
|
503 -a select all sessions |
|
504 -d DIR include session directory |
|
505 -g NAME select session group NAME |
|
506 -i incremental update according to session graph structure |
|
507 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
508 -v verbose |
|
509 -x NAME exclude session NAME and all descendants |
|
510 |
|
511 Maintain theory imports wrt. session structure. At least one operation |
|
512 needs to be specified (see options -I -M -U).\<close>} |
|
513 |
|
514 \<^medskip> |
|
515 The selection of sessions and session directories works as for @{tool build} |
|
516 via options \<^verbatim>\<open>-B\<close>, \<^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 |
|
517 \secref{sec:tool-build}). |
|
518 |
|
519 \<^medskip> |
|
520 Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build} |
|
521 (see \secref{sec:tool-build}). |
|
522 |
|
523 \<^medskip> |
|
524 Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. |
|
525 |
|
526 \<^medskip> |
|
527 Option \<^verbatim>\<open>-I\<close> determines reports session imports: |
|
528 |
|
529 \<^descr>[Potential session imports] are derived from old-style use of theory |
|
530 files from other sessions via the directory structure. After declaring |
|
531 those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a |
|
532 proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For |
|
533 example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal |
|
534 \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions} |
|
535 \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry. |
|
536 |
|
537 \<^descr>[Actual session imports] are derived from the session qualifiers of all |
|
538 currently imported theories. This helps to minimize dependencies in the |
|
539 session import structure to what is actually required. |
|
540 |
|
541 \<^medskip> |
|
542 Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of |
|
543 the underlying session directories; non-repository directories are ignored. |
|
544 This helps to find files that are accidentally ignored, e.g.\ due to |
|
545 rearrangements of the session structure. |
|
546 |
|
547 \<^medskip> |
|
548 Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications |
|
549 to canonical session-qualified theory names, according to the theory name |
|
550 space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification. |
|
551 |
|
552 Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally, |
|
553 following to the session graph structure in bottom-up order. This may |
|
554 lead to more accurate results in complex session hierarchies. |
|
555 \<close> |
|
556 |
|
557 subsubsection \<open>Examples\<close> |
|
558 |
|
559 text \<open> |
|
560 Determine potential session imports for some project directory: |
|
561 @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>} |
|
562 |
|
563 \<^smallskip> |
|
564 Mercurial repository check for some project directory: |
|
565 @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>} |
|
566 |
|
567 \<^smallskip> |
|
568 Incremental update of theory imports for some project directory: |
|
569 @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>} |
|
570 \<close> |
|
571 |
|
572 |
|
573 section \<open>Retrieve theory exports \label{sec:tool-export}\<close> |
487 section \<open>Retrieve theory exports \label{sec:tool-export}\<close> |
574 |
488 |
575 text \<open> |
489 text \<open> |
576 The @{tool_def "export"} tool retrieves theory exports from the session |
490 The @{tool_def "export"} tool retrieves theory exports from the session |
577 database. Its command-line usage is: @{verbatim [display] |
491 database. Its command-line usage is: @{verbatim [display] |