Closed IgnoredAmbience closed 5 years ago
Would a dummy replace on the result of this command enough ? :
grep -r Coq_ ./ | cut -d ':' -f 1 | sort -u
:
./esprima-to-ast.js ./generator/js_of_ast.ml ./generator/tests/lambda/BinNums.ml ./generator/tests/lambda/Lambda.ml ./generator/TODO ./jsref/assembly.js ./jsref/Compare.js ./jsref/displayed_sources.js ./jsref/JsCommonAux.ml ./jsref/JsCommonAux.unlog.js ./jsref/JsCommon.ml ./jsref/JsCommon.unlog.js ./jsref/JsInit.ml ./jsref/JsInit.unlog.js ./jsref/JsInterpreter.log.js ./jsref/JsInterpreter.ml ./jsref/JsInterpreterMonads.ml ./jsref/JsInterpreterMonads.unlog.js ./jsref/JsInterpreter.pseudo.js ./jsref/JsInterpreter.ptoken.js ./jsref/JsInterpreter.token.js ./jsref/JsInterpreter.unlog.js ./jsref/JsInterpreterUtils.ml ./jsref/JsInterpreterUtils.unlog.js ./jsref/JsSyntaxAux.ml ./jsref/JsSyntaxAux.unlog.js ./jsref/JsSyntax.ml ./jsref/JsSyntax.unlog.js ./jsref/Prheap.ml ./jsref/README.md ./jsref/Run_js.ml ./jsref/Translate_syntax.ml ./navig-driver.js ./test/interpreter.js ./test/parser.js ./tools/convert_monads_to_ppx.php
or do i miss something ?
It might work, but it would only be a quick fix: there are different Coq extraction’s naming conventions, and they might change for different Coq version. Typically, the naming convention are different for “Recursive Extraction” and “Extraction Library” (see https://github.com/coq/coq/wiki/ExtractionNameTricks ). I believe that it would be better to try to avoid the situations making Coq generate these prefixes; typically by (un)capitalizing the Coq identifiers when needed. It might take some time, though. I believe that your quick fix might need some capitalization-fix anyway. My fear is that if at some stage we switch to another version of Coq, we would have a lot of things to update :-\
@Mbodin We don't need to generate these files again, we've already moved far from where they came from. They're just the starting point for our OCaml interpreter.
You should run this command in a cleaned directory: no need to edit .unlog.js and .psuedo.js files as they're built from .ml.
Initial character of the remaining type name will need capitalising to pass OCaml's case-sensitivity rules?
I pushed a remove_coq_prefix. It may not be perfect since i still have some issue with the test suite. If you want to take a look it's there
Fixed by #32.
Note: also hardcoded in driver and test/*.js and generator