Unable to use built-in implicitly defined functions (e.g., sin(x))

[wdsmth]

I'm using KeYmaera X 5.0.2 on a remote Linux server (Ubuntu 22.04.3 LTS, amd64 architecture) accessed from a local Mac M1. The IJCAR22 implicit function examples do not appear, only the Textbook and Beginner's Tutorial Examples. (https://keymaerax.org/keymaeraXfunc/ indicates "To begin, click on the Import button for IJCAR22 Implicit Definitions Examples to load pre-defined example models.")

I copied the Arctan Identity example from implicitdefinitions.kyx. Apparently built-in functions like sin, cos, are known to my instance of KeYmaera X:

There are no errors or other warnings, but upon clicking "New proof", an error about undefined symbols cos,sin appears:

(NB: Implicit definitions work; e.g., I can define my own versions of sin,cos: implicit Real sine(Real t), cosine(Real t) = {{sine:=0; cosine:=1; t:=0;}; {sine'=cosine, cosine'=-sine, t'=1}};. However, this isn't very robust due to limitations on using custom functions. For example, t=0 & sine(0)=0 & cosine(0)=1 & x=1-> [{x'=-(sine(t)),t'=1} triggers a Core error:

In contrast, t=0 & x=0 & xdot=1 -> [{x'=xdot, xdot'=-x, t'=1}]x<=1 proves automatically. In my limited experience with implicit definitions, automation seems to perform worse in general, even when no errors are thrown. For instance t=0 & sine(0)=0 & cosine(0)=1 -> [{t'=1}@invariant((sine(t))^2 + (cosine(t))^2=1)]sine(t)<=1 requires the invariant for Auto to succeed.)

Probably extraneous detail: While running, the GUI shows "KeYmaera X 5.0.2 (no network)." at the bottom left.

[EnguerrandPrebet]

If you only see the Textbook and the Beginner's Examples, it is likely that you have selected "Learner's Mode" when starting KeYmeara X for the first time. The other examples appear if you choose "Industry Mode". To reset it, you can delete the keymaerax.sqlite file in ~/.keymaerax. Be careful that it will delete the visible models you currently have, so do not forget to click "Export all" beforehand.

The file you mentioned (implicitdefinitions.kyx) imports sin and cos explicitly: import kyx.math.{cos,sin};. The parser was misleading in that regard, it has been fixed in the current release.