#20388: Fix the Magma interface to work with remote installations
-------------------------------------+-------------------------------------
Reporter: mmasdeu | Owner:
Type: defect | Status: needs_review
Priority: major | Milestone: sage-7.2
Component: interfaces: | Resolution:
optional | Merged in:
Keywords: magma, remote | Reviewers:
Authors: Marc Masdeu | Work issues:
Report Upstream: N/A | Commit:
Branch: | ce26d46998e1c1be16babab4225dc0f9e1dac281
u/mmasdeu/20388-fix | Stopgaps:
Dependencies: |
-------------------------------------+-------------------------------------
Comment (by vdelecroix):
Replying to [comment:34 nbruin]:
> Replying to [comment:27 vdelecroix]:
> > Not exactly, it is done the first time you use tab completion with
magma. And the message says that it is saved '''locally''' in
`.sage//magma_intrinsic_cache.sobj` (with two ugly slashes). Might be
better to make it parameters dependent because two magma versions might
have different namespaces, no? (anyway not for this ticket)
>
> No, that is the best place to save it because that's one of the few
(hopefully persistent) places where you might expect to have write access.
Two magma versions tend to have only subtly different namespaces by
default, so the enormous cost of trying to differentiate is probably not
offset by having slightly more accurate tab completion.
I was not complaining about the location, just about potential version
clashes. However, this seems to be completely broken (at least with magma
2.11.13 on my computer).
--
Ticket URL: <http://trac.sagemath.org/ticket/20388#comment:37>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/sage-trac.
For more options, visit https://groups.google.com/d/optout.
