From b5434bbfb9dcbe9a342e6840717d1dd3879470ed Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Tue, 12 Mar 2024 13:28:01 +0100 Subject: [PATCH 1/2] Fix concept macro invocations --- src/foundation-core/identity-types.lagda.md | 6 ++++-- .../whiskering-higher-homotopies-composition.lagda.md | 5 +++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md index c9deb7361a..e36fc57851 100644 --- a/src/foundation-core/identity-types.lagda.md +++ b/src/foundation-core/identity-types.lagda.md @@ -128,8 +128,10 @@ ind-Id x B b y refl = b The identity types form a weak groupoidal structure on types. Thus they come equipped with -{{#concept "concatenation" Disambiguation="identifications" Agda=concat]} `(x ＝ y) → (y ＝ z) → (x ＝ z)` and an -{{#concept "inverse" Disambiguation="identification" Agda=inv}} operation `(x ＝ y) → (y ＝ x)`. +{{#concept "concatenation" Disambiguation="identifications" Agda=concat}} +`(x ＝ y) → (y ＝ z) → (x ＝ z)` and an +{{#concept "inverse" Disambiguation="identification" Agda=inv}} operation +`(x ＝ y) → (y ＝ x)`. There are many more operations on identity types. Some of them are defined in [path algebra](foundation.path-algebra.md) and diff --git a/src/foundation/whiskering-higher-homotopies-composition.lagda.md b/src/foundation/whiskering-higher-homotopies-composition.lagda.md index 2970a34a1e..27db8cd6d1 100644 --- a/src/foundation/whiskering-higher-homotopies-composition.lagda.md +++ b/src/foundation/whiskering-higher-homotopies-composition.lagda.md @@ -37,8 +37,9 @@ by α x ↦ ap² h (α x). ``` -Similarly, the {{#concept "right whiskering" Disambiguation="2-homotopies with -respect to composition" Agda=right-whisker-comp²}} is defined to be the operation +Similarly, the +{{#concept "right whiskering" Disambiguation="2-homotopies with respect to composition" Agda=right-whisker-comp²}} +is defined to be the operation ```text (H ~ H') → (h : (x : A) → B x) → (H ·r h ~ H' ·r h) From 60681b831bbdf0057e2914278aefae082f74df67 Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Tue, 12 Mar 2024 14:27:08 +0100 Subject: [PATCH 2/2] Recognize unparsed concept macros and fail the build --- scripts/preprocessor_concepts.py | 47 +++++++++++++++++++++++--------- 1 file changed, 34 insertions(+), 13 deletions(-) diff --git a/scripts/preprocessor_concepts.py b/scripts/preprocessor_concepts.py index b37a6dba09..85a83c1e15 100644 --- a/scripts/preprocessor_concepts.py +++ b/scripts/preprocessor_concepts.py @@ -26,7 +26,9 @@ r'\[(.*?)\]\(.*\)') EXTERNAL_LINKS_REGEX = re.compile( - r'## External links\s+', re.MULTILINE) + r'## External links\s+') + +LEFTOVER_CONCEPT_REGEX = re.compile(r'\{\{#concept.*') def make_definition_regex(definition): @@ -35,7 +37,7 @@ def make_definition_regex(definition): def does_support(backend): - return backend == 'html' + return backend == 'html' or backend == 'linkcheck' def match_wikidata_id(meta_text): @@ -82,7 +84,7 @@ def sup_link_reference(href, content, brackets=True, new_tab=False): return f'{brackets * "["}{content}{brackets * "]"}' -def sub_match_for_concept(m, mut_index, config, path, initial_content): +def sub_match_for_concept(m, mut_index, mut_error_locations, config, path, initial_content): text = m.group(1) metadata = m.group(2) wikidata_id = match_wikidata_id(metadata) @@ -118,8 +120,10 @@ def sub_match_for_concept(m, mut_index, config, path, initial_content): # TODO: decide if we want this # references.append(sup_link_reference(destination, 'AG')) else: - eprint('Concept definition not found:', plaintext, - '; expected', agda_name, 'to exist in', path) + eprint('Warning: Concept definition not found:', + plaintext, '; expected', agda_name, 'to exist in', + path) + mut_error_locations.add(path) anchor += f'' index_entry['link'] = f'{url_path}#{target_id}' # For now the link is the best thing we have as an identifier @@ -134,12 +138,19 @@ def sub_match_for_concept(m, mut_index, config, path, initial_content): return f'{anchor}{text}{"".join(reversed(references))}' -def tag_concepts_chapter_rec_mut(chapter, config, mut_index): +def tag_concepts_chapter_rec_mut(chapter, config, mut_index, mut_error_locations): mut_local_index = [] chapter['content'] = CONCEPT_REGEX.sub( lambda m: sub_match_for_concept( - m, mut_local_index, config, chapter['path'], chapter['content']), + m, mut_local_index, mut_error_locations, config, chapter['path'], chapter['content']), chapter['content']) + leftover_concepts = LEFTOVER_CONCEPT_REGEX.findall(chapter['content']) + if len(leftover_concepts) != 0: + eprint( + f'Warning: the following concept invocations were not recognized in {chapter["path"]}:') + mut_error_locations.add(chapter['path']) + for line in leftover_concepts: + eprint(' ' + line) external_references = [] for entry in mut_local_index: wikidata_label = entry.pop('__wikidata_label', None) @@ -166,22 +177,25 @@ def tag_concepts_chapter_rec_mut(chapter, config, mut_index): formatted_references + chapter['content'][insert_at:] else: chapter['content'] += f'\n## External links\n\n{formatted_references}' - tag_concepts_sections_rec_mut(chapter['sub_items'], config, mut_index) + tag_concepts_sections_rec_mut( + chapter['sub_items'], config, mut_index, mut_error_locations) -def tag_concepts_sections_rec_mut(sections, config, mut_index): +def tag_concepts_sections_rec_mut(sections, config, mut_index, mut_error_locations): for section in sections: chapter = section.get('Chapter') if chapter is None: continue - tag_concepts_chapter_rec_mut(chapter, config, mut_index) + tag_concepts_chapter_rec_mut( + chapter, config, mut_index, mut_error_locations) -def tag_concepts_root_section(section, config, mut_index): +def tag_concepts_root_section(section, config, mut_index, mut_error_locations): chapter = section.get('Chapter') if chapter is not None: - tag_concepts_chapter_rec_mut(chapter, config, mut_index) + tag_concepts_chapter_rec_mut( + chapter, config, mut_index, mut_error_locations) return section @@ -203,10 +217,17 @@ def tag_concepts_root_section(section, config, mut_index): # Thread the index through execution mut_index = [] + mut_error_locations = set() if bool(concepts_config.get('enable', True)) == True: book['sections'] = list(map( - lambda s: tag_concepts_root_section(s, concepts_config, mut_index), + lambda s: tag_concepts_root_section( + s, concepts_config, mut_index, mut_error_locations), book['sections'])) + if len(mut_error_locations) != 0: + eprint('The following files contain errors:') + for location in mut_error_locations: + eprint(' ' + location) + sys.exit(1) else: eprint('Skipping concept tagging, enable option was set to', concepts_config.get('enable'))