2d:null 2e:["$","title",null,{"children":"GitHub Lean doc preview | Bryan Gin-ge Chen | Observable"}] 33:T1170,viewof urls = { const exampleFileURL = 'https://github.com/leanprover-community/mathlib/blob/9f0687c721823eafa6a58c1137afbc80302470dd/src/number_theory/bernoulli.lean'; const examplePRURL = 'https://github.com/leanprover-community/mathlib/pull/1716/'; const examplePRNumber = '1716'; const output = html``; const exampleSingle = html`${exampleFileURL}`; const examplePR = html`${examplePRURL}`; const exampleNumber = html`${examplePRNumber}`; const form = html`

${output}

Input one of the following:

a GitHub URL to a single Lean file (e.g. ${exampleSingle})
a GitHub URL to a PR involving .lean files (e.g. ${examplePR})
a mathlib PR number (e.g. ${exampleNumber})

and then hit enter or unfocus the box. `; exampleSingle.onclick = () => { form.text.value = exampleFileURL; form.text.onchange(); }; examplePR.onclick = () => { form.text.value = examplePRURL; form.text.onchange(); }; exampleNumber.onclick = () => { form.text.value = examplePRNumber; form.text.onchange(); }; form.text.oninput = e => { e.stopPropagation(); }; function getUrlsFromPR(pr, repo, inputUrl) { // https://developer.github.com/v3/pulls/#list-pull-requests-files const ghUrl = `https://api.github.com/repos/${repo}/pulls/${pr}/files?per_page=100`; fetch(ghUrl) .then(res => { if (res.headers.has('link')) { // multiple pages! see https://developer.github.com/v3/guides/traversing-with-pagination/ const pages = parseInt( res.headers.get('link').match(/page=(\d+)>; rel="last"$/)[1] ); return res.json().then(async files => { const pageFiles = await Promise.all( Array.from({ length: pages - 1 }, (_, i) => fetch(ghUrl + `&page=${i + 2}`).then(res => res.json()) ) ); return [files, pageFiles].flat(2); }); } else return res.json(); }) .then(files => { if (files.message) { if (files.message === 'Not Found') output.value = `Could not find PR corresponding to: ${inputUrl}`; else output.value = files.message; form.text.style.backgroundColor = 'pink'; } else { form.value = files .map(({ blob_url }) => ({ url: blob_url, anchor: html`^` })) .filter(({ url }) => url.endsWith('.lean')); form.value.url = inputUrl; form.dispatchEvent(new CustomEvent('input')); form.text.style.backgroundColor = 'initial'; output.value = ''; } }) .catch(e => { output.value = e; form.text.style.backgroundColor = 'pink'; }); } form.text.onchange = () => { const value = form.text.value; if (value.startsWith('https://github.com/')) { if (value.match(/\/pull\//)) { const arr = value.split('/'); const repo = arr.slice(3, 5).join('/'); const pr = parseInt(arr[6]); getUrlsFromPR(pr, repo, arr.slice(0, 7).join('/')); } else { form.value = [{ url: value, anchor: html`^` }]; form.value.url = value; form.dispatchEvent(new CustomEvent('input')); form.text.style.backgroundColor = 'initial'; output.value = ''; } } else if (!isNaN(parseInt(value))) { getUrlsFromPR(parseInt(value), 'leanprover-community/mathlib', value); } else if (value.startsWith('https://gist.githubusercontent.com')) { form.value = [{ url: value, anchor: html`^` }]; form.value.url = value; form.dispatchEvent(new CustomEvent('input')); form.text.style.backgroundColor = 'initial'; output.value = ''; } else { output.value = `Could not parse "${value}" as a Lean file on GitHub, a PR on GitHub, or a number`; form.text.style.backgroundColor = 'pink'; } }; form.text.onchange(); form.onsubmit = e => e.preventDefault(); return form; }34:T6a1,function leanDocParser(input) { let currLine = 1; let { text, math } = removeMath(input, '$'); const docs = []; function eatToNext(re) { const i = text.search(re); let eaten; if (i === -1) { eaten = text; text = ''; } else { eaten = text.slice(0, i); text = text.slice(i); } currLine += eaten.split('\n').length - 1; return eaten; } function eatBlockComment() { let nest = 1; let doc = ""; while (nest > 0) { doc += eatToNext(blockRE); if (text.slice(0, 2) === '/-') { nest++; doc += '/-'; } else { nest--; doc += nest > 0 ? '-/' : ''; } text = text.slice(2); } return doc; } const anyCommentRE = new RegExp('--|/-'); const blockRE = new RegExp('/-|-/'); const closeCommentRE = new RegExp('-/'); let N = 0; while (text.length && ++N < 1000) { eatToNext(anyCommentRE); if (text.slice(0, 2) === '--') { eatToNext('\n'); text = text.slice(1); currLine++; } else if (text.slice(0, 2) === '/-') { text = text.slice(2); if (text[0] === '!') { text = text.slice(1); const line = currLine; const moduleDocString = eatBlockComment(); docs.push({ type: 'module docstring', line, doc: moduleDocString }); } else if (text[0] === '-') { text = text.slice(1); const line = currLine; const docString = eatBlockComment(); docs.push({ type: 'docstring', line, doc: docString }); } else { eatBlockComment(); } } } return { docs, math }; }35:T6ac,MathJax = { if (document.getElementById('mathjax')) { return window.MathJax; } let trigger; const ready = new Promise(res => (trigger = res)); // cf. https://github.com/leanprover-community/doc-gen/blob/master/print_docs.py#L279 window.MathJax = { tex: { inlineMath: [['$', '$']], displayMath: [['$$', '$$']] }, options: { skipHtmlTags: [ 'script', 'noscript', 'style', 'textarea', 'pre', 'code', 'annotation', 'annotation-xml', 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name', 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields', 'constructor', 'constructors', 'instances' ], ignoreHtmlClass: 'tex2jax_ignore', processHtmlClass: 'tex2jax_process' }, // http://docs.mathjax.org/en/latest/web/configuration.html#performing-actions-during-initialization startup: { ready: () => { // console.log('MathJax is loaded, but not yet initialized'); window.MathJax.startup.defaultReady(); trigger(); // console.log('MathJax is initialized, and the initial typeset is queued'); } } }; // http://docs.mathjax.org/en/latest/web/configuration.html#configuring-and-loading-in-one-script (function() { var script = document.createElement('script'); script.id = 'mathjax'; script.src = 'https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js'; script.async = true; document.head.appendChild(script); })(); await ready; return window.MathJax; }36:T5a7,md`## Version history - [2019/11/23](https://observablehq.com/@bryangingechen/github-lean-doc-preview@535): first publish - [2020/02/05](https://observablehq.com/@bryangingechen/github-lean-doc-preview@592): added MathJax support ([test case](https://observablehq.com/@bryangingechen/github-lean-doc-preview?url=%221952%22)) - [2020/03/14](https://observablehq.com/@bryangingechen/github-lean-doc-preview@625): change [comment parsing for Lean 3.6.0](https://github.com/leanprover-community/lean/blob/master/doc/changes.md#v360c-26-feb-2020) ([test case](https://observablehq.com/@bryangingechen/github-lean-doc-preview?url=%22https%3A%2F%2Fgithub.com%2Fbryangingechen%2Flean%2Fblob%2Ffe763ae78ac508b37beed14ef81fa4087ba75e2c%2Ftests%2Flean%2Frun%2Fcomment.lean%22#docs)). (This could break highlighting of certain files; let me know if this is a big problem and I can add a toggle.) Also added Lean syntax highlighting (courtesy of [Patrick Massot's highlightjs code](https://observablehq.com/@bryangingechen/highlightjs-for-lean)) for code blocks in docstrings ([test case](https://observablehq.com/@bryangingechen/github-lean-doc-preview?url=%22https%3A%2F%2Fgithub.com%2Fleanprover-community%2Fmathlib%2Fblob%2Fmaster%2Fsrc%2Ftactic%2Fsubtype_instance.lean%22#docs)). - [2020/06/24](https://observablehq.com/@bryangingechen/github-lean-doc-preview@627): Fix broken links - 2021/02/15: support raw gist URLs, switch markdown+mathjax handling. `37:[] 31:{"id":"5a19aff044979843","slug":"github-lean-doc-preview","title":"GitHub Lean doc preview","thumbnail":"eaca74705c6742c199af3dc188ecdd29e1b8d2dceb72b73a38f3f738fa6079e0","access_level":"public","create_time":"$D2019-11-12T21:29:18.945Z","update_time":"$D2021-02-16T01:23:52.880Z","view_time":null,"first_public_time":"$D2019-11-23T05:26:17.486Z","fork":false,"stars":4,"starred":false,"owner":{"type":"team","id":"d2fd23101beb2a61","login":"bryangingechen","name":"Bryan Gin-ge Chen","avatar_url":"https://avatars-next.observableusercontent.com/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","tier":"starter_2024"},"version":675,"publish_version":675,"role":null,"authored":false,"authors":[{"type":"individual","id":"5c13a1a27cf52564","login":"bryangingechen","name":"Bryan Gin-ge Chen","avatar_url":"https://avatars-next.observableusercontent.com/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","tier":null}],"members":[{"type":"individual","id":"5c13a1a27cf52564","login":"bryangingechen","name":"Bryan Gin-ge Chen","avatar_url":"https://avatars-next.observableusercontent.com/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","tier":null,"role":"editor"}],"comments":[],"custom_thumbnail":false,"trashed":false,"subscribed":null,"forks":2,"collection":{"id":"68b035771823d0b5","slug":"lean","title":"Lean","owner":{"id":"d2fd23101beb2a61","login":"bryangingechen","name":"Bryan Gin-ge Chen"}},"type":"notebook","body":{"title":"GitHub Lean doc preview","cells":[{"id":0,"value":"md`# GitHub Lean doc preview\n\n*See also: [the Github Lean file viewer](https://observablehq.com/@bryangingechen/github-lean-file-viewer).*\n\nQuickly preview all the docstrings in a [Lean](https://leanprover.github.io) file hosted on GitHub or check the rendering of the docstrings in a PR to your favorite Lean repo!\n\nNote that getting the list of changed files from GitHub uses the GitHub API, and this is [rate-limited](https://developer.github.com/v3/#rate-limiting) to 60 requests per hour.\n\nFurther note that this page uses (a relatively old version of) the [\\`marked\\`](https://github.com/markedjs/marked) library to typeset markdown, so the results may differ from what you see on e.g. [the official mathlib doc page](https://leanprover-community.github.io/mathlib_docs/).`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined"},{"id":4,"value":"$33","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined"},{"id":164,"value":"md`## [🔗 Permalink](${permalink({ url: urls.url })}#docs)\n------`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined"},{"id":380,"value":"toc = html`\n${viewof page}\n

${anchor} ${url}