Stream: Coq users

Topic: ✔ interval 4.3.0 plotting failure


view this post on Zulip Ben Siraphob (Jul 27 2021 at 16:12):

I'm testing out the interval package with certified plotting support but the plotting fails on macOS:
cc @Guillaume Melquiond @Vincent Semeria

$ coqtop
Welcome to Coq 8.12.2 (January 1980)

Coq < From Coq Require Import Reals.
[Loading ML file newring_plugin.cmxs ... done]
[Loading ML file r_syntax_plugin.cmxs ... done]
[Loading ML file zify_plugin.cmxs ... done]
[Loading ML file micromega_plugin.cmxs ... done]

Coq < From Interval Require Import Plot Tactic.
[Loading ML file interval_plot.cmxs ... done]
[Loading ML file omega_plugin.cmxs ... done]
[Loading ML file ssrmatching_plugin.cmxs ... done]
[Loading ML file ssreflect_plugin.cmxs ... done]
[Loading ML file int63_syntax_plugin.cmxs ... done]
[Loading ML file float_syntax_plugin.cmxs ... done]
[Loading ML file bignums_syntax_plugin.cmxs ... done]

Coq < Open Scope R_scope.

Coq < Definition p1 := ltac:(plot (fun x => x^2 * sin (x^2)) (-4) 4).
p1 is defined

Coq < Plot p1.

Coq < WARNING: Plotting with an 'unknown' terminal.
No output will be generated. Please select a terminal with 'set terminal'.
"/tmp/interval_plotad5922" line 521: undefined variable: mouse

view this post on Zulip Ben Siraphob (Jul 28 2021 at 06:18):

This was answered on Zulip

view this post on Zulip Ben Siraphob (Jul 28 2021 at 06:18):

Screen-Shot-2021-07-28-at-13.18.52.png

view this post on Zulip Notification Bot (Jul 28 2021 at 06:19):

Ben Siraphob has marked this topic as resolved.


Last updated: Jan 31 2023 at 13:02 UTC