rudimentary documentation test
authorhaftmann
Wed Mar 14 17:40:00 2012 +0100 (2012-03-14)
changeset 4693489cc3dfb383b
parent 46933 3b02b0ef8d48
child 46936 571ce2bc0b64
rudimentary documentation test
Admin/mira.py
     1.1 --- a/Admin/mira.py	Wed Mar 14 15:54:54 2012 +0100
     1.2 +++ b/Admin/mira.py	Wed Mar 14 17:40:00 2012 +0100
     1.3 @@ -257,6 +257,21 @@
     1.4      """HOL image"""
     1.5      return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
     1.6  
     1.7 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
     1.8 +def HOL_Library(*args):
     1.9 +    """HOL-Library image"""
    1.10 +    return build_isabelle_image('HOL', 'HOL', 'HOL-Library', *args)
    1.11 +
    1.12 +@configuration(repos = [Isabelle], deps = [(Pure, [0])])
    1.13 +def ZF(*args):
    1.14 +    """ZF image"""
    1.15 +    return build_isabelle_image('ZF', 'Pure', 'ZF', *args)
    1.16 +
    1.17 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
    1.18 +def HOL_HOLCF(*args):
    1.19 +    """HOLCF image"""
    1.20 +    return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args)
    1.21 +
    1.22  @configuration(repos = [Isabelle], deps = [(Pure_64, [0])])
    1.23  def HOL_64(*args):
    1.24      """HOL image (64 bit)"""
    1.25 @@ -293,19 +308,39 @@
    1.26      return isabelle_makeall(*args)
    1.27  
    1.28  
    1.29 -# Document and Distribution Build
    1.30 +# distribution and documentation Build
    1.31  
    1.32  @configuration(repos = [Isabelle], deps = [])
    1.33  def Distribution(env, case, paths, dep_paths, playground):
    1.34 -    """Document and Distribution Build"""
    1.35 +    """Build of distribution"""
    1.36      ## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly
    1.37      isabelle_home = paths[0]
    1.38 -    makedist = path.join(isabelle_home, 'Admin', 'makedist')
    1.39 -    (return_code, log) = env.run_process(makedist,
    1.40 +    (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'makedist'),
    1.41        REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd())
    1.42      return (return_code == 0, '', ## FIXME might add summary here
    1.43        {}, {'log': log}, None) ## FIXME might add proper result here
    1.44  
    1.45 +@configuration(repos = [Isabelle], deps = [
    1.46 +    (HOL, [0]),
    1.47 +    (HOL_HOLCF, [0]),
    1.48 +    (ZF, [0]),
    1.49 +    (HOL_Library, [0])
    1.50 +  ])
    1.51 +def Documentation_images(*args):
    1.52 +    """Isabelle images needed to build the documentation"""
    1.53 +    return isabelle_dependency_only(*args)
    1.54 +
    1.55 +@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])])
    1.56 +def Documentation(env, case, paths, dep_paths, playground):
    1.57 +    """Build of documentation"""
    1.58 +    isabelle_home = paths[0]
    1.59 +    dep_path = dep_paths[0]
    1.60 +    prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
    1.61 +      usedir_options = default_usedir_options)
    1.62 +    (return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src'))
    1.63 +    return (return_code == 0, extract_isabelle_run_summary(log),
    1.64 +      extract_report_data(isabelle_home, log), {'log': log}, None)
    1.65 +
    1.66  
    1.67  # Mutabelle configurations
    1.68