chore: snake-case attributes

[digama0]

As discussed in this week's dev meeting, this renames all attributes to use the snake-case convention. More specifically and for future reference, the following attributes have been renamed:

alwaysInline -> always_inline
appUnexpander -> app_unexpander
attrParser -> attr_parser
builtinAttrParser -> builtin_attr_parser
builtinCategoryParenthesizer -> builtin_category_parenthesizer
builtinCommandElab -> builtin_command_elab
builtinCommandParser -> builtin_command_parser
builtinDelab -> builtin_delab
builtinDoElemParser -> builtin_doElem_parser
builtinFormatter -> builtin_formatter
builtinInit -> builtin_init
builtinLevelParser -> builtin_level_parser
builtinMacro -> builtin_macro
builtinMissingDocsHandler -> builtin_missing_docs_handler
builtinParenthesizer -> builtin_parenthesizer
builtinPrecParser -> builtin_prec_parser
builtinPrioParser -> builtin_prio_parser
builtinQuotPrecheck -> builtin_quot_precheck
builtinSyntaxParser -> builtin_syntax_parser
builtinTactic -> builtin_tactic
builtinTacticParser -> builtin_tactic_parser
builtinTermElab -> builtin_term_elab
builtinTermParser -> builtin_term_parser
categoryParenthesizer -> category_parenthesizer
combinatorFormatter -> combinator_formatter
combinatorParenthesizer -> combinator_parenthesizer
commandElab -> command_elab
commandParser -> command_parser
computedField -> computed_field
defaultInstance -> default_instance
doElemParser -> doElem_parser
elabAsElim -> elab_as_elim
elabWithoutExpectedType -> elab_without_expected_type
implementedBy -> implemented_by
inferTCGoalsRL -> infer_tc_goals_rl
inheritDoc -> inherit_doc
inlineIfReduce -> inline_if_reduce
macroInline -> macro_inline
matchPattern -> match_pattern
missingDocsHandler -> missing_docs_handler
neverExtract -> never_extract
precParser -> prec_parser
prioParser -> prio_parser
quotPrecheck -> quot_precheck
runBuiltinParserAttributeHooks -> run_builtin_parser_attribute_hooks
runParserAttributeHooks -> run_parser_attribute_hooks
serverRpcMethod -> server_rpc_method
stxParser -> stx_parser
tacticParser -> tactic_parser
termElab -> term_elab
termParser -> term_parser
unificationHint -> unification_hint
unusedVariablesIgnoreFn -> unused_variables_ignore_fn

The lake attributes have also been renamed, for consistency:

defaultTarget -> default_target
externLib -> extern_lib
leanExe -> lean_exe
leanLib -> lean_lib
libraryFacet -> library_facet
moduleFacet -> module_facet
packageDep -> package_dep
packageFacet -> package_facet

[digama0]

This is a minor bug fix that was revealed by the refactor.

[digama0]

I would rather not snake case the definition, but this is required due to a peculiarity in the way attributes are looked up - the parser kind has its namespaces stripped and this has to match the name of the attribute as entered into the attribute map. Refactoring this is probably best left for a future PR though.

[digama0]

The reason this attribute is not completely snake cased (although I suppose it looks fine as is) is because elab_rules and macro_rules make the assumption that you can just stick Parser (now _parser) at the end of the category name to derive the parser attribute name. So this function is somewhat misleading and should probably not have the first argument at all, to avoid the implication that it can be changed.

[digama0]

The nix build is failing due to breakage in LeanInk, which I didn't realize was a dependency. How are changes in LeanInk tracked? Why isn't it also a submodule like Lake? I'm not really sure how to update that in concert with everything else.

[gebner]

How are changes in LeanInk tracked?

The LeanInk revision is specified in the flake.lock file for Nix. You can update it with nix flake update.

I must warn you that I have put a small hack in the lockfile¹: the lockfile refers to my personal fork, while the flake.nix file says leanprover/LeanInk. 😄 I should probably ask for write access to that repo to merge leanprover/LeanInk#36

¹ Nix makes that very easy with nix flake update --override-input leanInk github:gebner/LeanInk/impldetailhyp.

[digama0]

@gebner I don't suppose I can ask you to do that? I don't have or use nix at all, and while I was hoping to find/replace your commit in the lockfile for my commit (leanprover/LeanInk#37), I can find neither your commit nor indeed LeanInk at all in the flake.lock file.

[gebner]

I can find neither your commit

Oh, I think I force-pushed a fix to that branch before merging the PR but forgot about updating the lockfile. Now I'm kinda surprised that it still builds.. Maybe it's stored in cachix?

I've pushed a flake.lock "update."

[leodemoura]

@gebner Any pending issues? If not, let's merge before the PR rots.

[gebner]

👍 for merging this PR before it rots. We should merge the accumulated LeanInk PRs though (I'd do it myself if I could).