I am creating presentation slides using beamer, and on the slides I want to include pieces of code from Agda and Isabelle standard libraries. All I can find online is generating latex from Agda (lagda) or from Isabelle (document preparation). I want to go the other way, as my slides will have code from different systems. I can still use lstlisting or verbatim, but I would rather not copy-paste and reformat code.
I would prefer to have something like including line numbers from files, or maybe code between tags
Your best bet is to use the catchfilebetweentags package: given two files IsabelleCode.tex and AgdaCode.tex generated by the respective LaTeX backends of each language, you can capture the code between an opening tag %<*TAGNAME> and a closing tag %</TAGNAME> in either file by using the appropriate directive e.g.:
\ExecuteMetaData[IsabelleCode.tex]{TAGNAME}
\ExecuteMetaData[AgdaCode.tex]{TAGNAME}
Does this package compiles the agda/isabelle source code every time the latex file is compiled?
No. It does not know anything about Agda / Isabelle. You have to write a sensible Makefile to organise your dependencies and rebuild the .tex files when the source Isabelle / Agda is modified.